Theorem biUnion_Ici_eq_Ici_iff

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 biUnion_Ici_eq_Ici_iff View on Github →