mathlib3 documentation

topology.algebra.order.upper_lower

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 provide has_upper_lower_closure, an ad hoc axiomatisation of the properties we need.

source
@[class]
structure has_upper_lower_closure (α : Type u_1) [topological_space α] [preorder α] :
Prop

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!

Instances of this typeclass
source
@[protected, instance]
def ordered_comm_group.to_has_upper_lower_closure {α : Type u_1} [topological_space α] [ordered_comm_group α] [has_continuous_const_smul α α] :
has_upper_lower_closure α
source
@[protected, instance]
def ordered_add_comm_group.to_has_upper_lower_closure {α : Type u_1} [topological_space α] [ordered_add_comm_group α] [has_continuous_const_vadd α α] :
has_upper_lower_closure α
source
@[simp]
theorem upper_bounds_closure {α : Type u_1} [topological_space α] [preorder α] [order_closed_topology α] (s : set α) :
upper_bounds (closure s) = upper_bounds s
source
@[simp]
theorem lower_bounds_closure {α : Type u_1} [topological_space α] [preorder α] [order_closed_topology α] (s : set α) :
lower_bounds (closure s) = lower_bounds s
source
@[simp]
theorem bdd_above_closure {α : Type u_1} [topological_space α] [preorder α] [order_closed_topology α] {s : set α} :
bdd_above (closure s) ↔ bdd_above s
source
@[simp]
theorem bdd_below_closure {α : Type u_1} [topological_space α] [preorder α] [order_closed_topology α] {s : set α} :
bdd_below (closure s) ↔ bdd_below s
source
theorem bdd_above.of_closure {α : Type u_1} [topological_space α] [preorder α] [order_closed_topology α] {s : set α} :
bdd_above (closure s) → bdd_above s

Alias of the forward direction of bdd_above_closure.

source
@[protected]
theorem bdd_above.closure {α : Type u_1} [topological_space α] [preorder α] [order_closed_topology α] {s : set α} :
bdd_above s → bdd_above (closure s)

Alias of the reverse direction of bdd_above_closure.

source
@[protected]
theorem bdd_below.closure {α : Type u_1} [topological_space α] [preorder α] [order_closed_topology α] {s : set α} :
bdd_below s → bdd_below (closure s)

Alias of the reverse direction of bdd_below_closure.

source
theorem bdd_below.of_closure {α : Type u_1} [topological_space α] [preorder α] [order_closed_topology α] {s : set α} :
bdd_below (closure s) → bdd_below s

Alias of the forward direction of bdd_below_closure.

source
@[protected]
theorem is_upper_set.closure {α : Type u_1} [topological_space α] [preorder α] [has_upper_lower_closure α] {s : set α} :
is_upper_set s → is_upper_set (closure s)
source
@[protected]
theorem is_lower_set.closure {α : Type u_1} [topological_space α] [preorder α] [has_upper_lower_closure α] {s : set α} :
is_lower_set s → is_lower_set (closure s)
source
@[protected]
theorem is_open.upper_closure {α : Type u_1} [topological_space α] [preorder α] [has_upper_lower_closure α] {s : set α} :
is_open s → is_open ↑(upper_closure s)
source
@[protected]
theorem is_open.lower_closure {α : Type u_1} [topological_space α] [preorder α] [has_upper_lower_closure α] {s : set α} :
is_open s → is_open ↑(lower_closure s)
source
@[protected, instance]
def order_dual.has_upper_lower_closure {α : Type u_1} [topological_space α] [preorder α] [has_upper_lower_closure α] :
has_upper_lower_closure αᵒᵈ
source
@[protected]
theorem is_upper_set.interior {α : Type u_1} [topological_space α] [preorder α] [has_upper_lower_closure α] {s : set α} (h : is_upper_set s) :
is_upper_set (interior s)
source
@[protected]
theorem is_lower_set.interior {α : Type u_1} [topological_space α] [preorder α] [has_upper_lower_closure α] {s : set α} (h : is_lower_set s) :
is_lower_set (interior s)
source
@[protected]
theorem set.ord_connected.interior {α : Type u_1} [topological_space α] [preorder α] [has_upper_lower_closure α] {s : set α} (h : s.ord_connected) :
(interior s).ord_connected