Topological facts about upper/lower/order-connected sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The topological closure and interior of an upper/lower/order-connected set is an upper/lower/order-connected set (with the notable exception of the closure of an order-connected set).
Implementation notes #
The same lemmas are true in the additive/multiplicative worlds. To avoid code duplication, we
has_upper_lower_closure, an ad hoc axiomatisation of the properties we need.
- is_upper_set_closure : ∀ (s : set α), is_upper_set s → is_upper_set (closure s)
- is_lower_set_closure : ∀ (s : set α), is_lower_set s → is_lower_set (closure s)
- is_open_upper_closure : ∀ (s : set α), is_open s → is_open ↑(upper_closure s)
- is_open_lower_closure : ∀ (s : set α), is_open s → is_open ↑(lower_closure s)
Ad hoc class stating that the closure of an upper set is an upper set. This is used to state lemmas that do not mention algebraic operations for both the additive and multiplicative versions simultaneously. If you find a satisfying replacement for this typeclass, please remove it!