Theorem IsGLB.isLeast

Modification history

2026-08-15 17:29

Mathlib/Order/Bounds/Basic.lean

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

Added IsGLB.isLeast View on Github →