Commit 2026-04-13 06:55 c773983e

View on Github →

chore(Data/Set/Finite/Lattice): use to_dual (#37051)

Estimated changes

Modified Mathlib/Data/Set/Finite/Lattice.lean

deleted theorem Set.Finite.bddBelow_biUnion

deleted theorem Set.Finite.iInf_biSup_of_antitone

deleted theorem Set.Finite.iInf_biSup_of_monotone

deleted theorem Set.infinite_of_not_bddBelow

deleted theorem Set.map_finite_biInf

deleted theorem Set.map_finite_iInf

deleted theorem iInf_iSup_of_antitone

deleted theorem iInf_iSup_of_monotone

Modified Mathlib/Order/CompleteBooleanAlgebra.lean