Theorem isLeast_iff_isGLB_and_mem

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 isLeast_iff_isGLB_and_memView on Github →