Theorem IsLeast.biUnion_Ici_eq_Ici

Modification history

2026-08-15 17:29

Mathlib/Order/Interval/Set/Disjoint.lean

feat(Order/Interval/Set/Disjoint): generalize `⋃ x ∈ s, Iic x = Iic a` from `LinearOrder` to `Preorder` (#42512) …

Added IsLeast.biUnion_Ici_eq_Ici View on Github →