Topological facts about upper/lower/order-connected sets

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

class HasUpperLowerClosure (α : Type u_1) [TopologicalSpace α] [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!

• isUpperSet_closure : ∀ (s : Set α), IsUpperSet s → IsUpperSet (closure s)
• isLowerSet_closure : ∀ (s : Set α), IsLowerSet s → IsLowerSet (closure s)
• isOpen_upperClosure : ∀ (s : Set α), IsOpen s → IsOpen ↑(upperClosure s)
• isOpen_lowerClosure : ∀ (s : Set α), IsOpen s → IsOpen ↑(lowerClosure s)

theorem HasUpperLowerClosure.isUpperSet_closure {α : Type u_1} : ∀ {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : HasUpperLowerClosure α] (s : Set α), IsUpperSet s → IsUpperSet (closure s)

theorem HasUpperLowerClosure.isLowerSet_closure {α : Type u_1} : ∀ {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : HasUpperLowerClosure α] (s : Set α), IsLowerSet s → IsLowerSet (closure s)

theorem HasUpperLowerClosure.isOpen_upperClosure {α : Type u_1} : ∀ {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : HasUpperLowerClosure α] (s : Set α), IsOpen s → IsOpen ↑(upperClosure s)

theorem HasUpperLowerClosure.isOpen_lowerClosure {α : Type u_1} : ∀ {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : HasUpperLowerClosure α] (s : Set α), IsOpen s → IsOpen ↑(lowerClosure s)

@[instance 100]

instance OrderedAddCommGroup.to_hasUpperLowerClosure {α : Type u_1} [TopologicalSpace α] [OrderedAddCommGroup α] [ContinuousConstVAdd α α] : HasUpperLowerClosure α

Equations

• ⋯ = ⋯

@[instance 100]

instance OrderedCommGroup.to_hasUpperLowerClosure {α : Type u_1} [TopologicalSpace α] [OrderedCommGroup α] [ContinuousConstSMul α α] : HasUpperLowerClosure α

Equations

• ⋯ = ⋯

theorem IsUpperSet.closure {α : Type u_1} [TopologicalSpace α] [Preorder α] [HasUpperLowerClosure α] {s : Set α} : IsUpperSet s → IsUpperSet (closure s)

theorem IsLowerSet.closure {α : Type u_1} [TopologicalSpace α] [Preorder α] [HasUpperLowerClosure α] {s : Set α} : IsLowerSet s → IsLowerSet (closure s)

theorem IsOpen.upperClosure {α : Type u_1} [TopologicalSpace α] [Preorder α] [HasUpperLowerClosure α] {s : Set α} : IsOpen s → IsOpen ↑(upperClosure s)

theorem IsOpen.lowerClosure {α : Type u_1} [TopologicalSpace α] [Preorder α] [HasUpperLowerClosure α] {s : Set α} : IsOpen s → IsOpen ↑(lowerClosure s)

instance instHasUpperLowerClosureOrderDual {α : Type u_1} [TopologicalSpace α] [Preorder α] [HasUpperLowerClosure α] : HasUpperLowerClosure αᵒᵈ

Equations

• ⋯ = ⋯

theorem IsUpperSet.interior {α : Type u_1} [TopologicalSpace α] [Preorder α] [HasUpperLowerClosure α] {s : Set α} (h : IsUpperSet s) : IsUpperSet (interior s)

theorem IsLowerSet.interior {α : Type u_1} [TopologicalSpace α] [Preorder α] [HasUpperLowerClosure α] {s : Set α} (h : IsLowerSet s) : IsLowerSet (interior s)

theorem Set.OrdConnected.interior {α : Type u_1} [TopologicalSpace α] [Preorder α] [HasUpperLowerClosure α] {s : Set α} (h : s.OrdConnected) : (interior s).OrdConnected