Commit 2026-08-15 17:29 5e04dcab

View on Github →

feat(Order/Interval/Set/Disjoint): generalize ⋃ x ∈ s, Iic x = Iic a from LinearOrder to Preorder (#42512) and add an IsLeast version.

Estimated changes

Modified Mathlib/Order/Bounds/Basic.lean

added theorem IsGLB.isLeast

added theorem isLeast_iff_isGLB_and_mem

Modified Mathlib/Order/Interval/Set/Disjoint.lean

modified theorem IsGLB.biUnion_Ici_eq_Ici

deleted theorem IsLUB.biUnion_Iic_eq_Iic

added theorem IsLeast.biUnion_Ici_eq_Ici

added theorem biUnion_Ici_eq_Ici_iff

modified theorem iUnion_Ici_eq_Ici_iInf

modified theorem iUnion_Iic_eq_Iic_iSup