Commit 2024-11-15 11:45 e6b15a40

View on Github →

feat: ⋃ a ∈ s, t = t (#19029) ... when s is nonempty. Also remove the stray Sort _ in the complete lattice version of this lemma From GrowthInGroups

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.biInter_const

added theorem Set.biUnion_const

Modified Mathlib/Order/CompleteLattice.lean

modified theorem biInf_const

modified theorem biSup_const