Commit 2024-02-14 21:13 8f525447

View on Github →

feat(Topology/Order): assorted lemmas (#10556)

Add upperBounds_closure, lowerBounds_closure, bddAbove_closure, bddBelow_closure.
Add IsAntichain.interior_eq_empty.
Generalize nhds_left'_le_nhds_ne and nhds_right'_le_nhds_ne to a Preorder. Partly forward-ports https://github.com/leanprover-community/mathlib/pull/16976

Estimated changes

Modified Mathlib/Data/Set/Intervals/UnorderedInterval.lean

Modified Mathlib/Order/Bounds/Basic.lean

added theorem mem_lowerBounds_iff_subset_Ici

added theorem mem_upperBounds_iff_subset_Iic

Modified Mathlib/Topology/Algebra/Order/LeftRight.lean

added theorem IsAntichain.interior_eq_empty'

added theorem IsAntichain.interior_eq_empty

Modified Mathlib/Topology/Algebra/Order/UpperLower.lean

Modified Mathlib/Topology/Order/OrderClosed.lean

added theorem bddAbove_closure

added theorem bddBelow_closure

added theorem lowerBounds_closure

added theorem upperBounds_closure