Computational realization of topological spaces (experimental)

This file provides infrastructure to compute with topological spaces.

Main declarations

• Ctop: Realization of a topology basis.
• Ctop.Realizer: Realization of a topological space. Ctop that generates the given topology.
• LocallyFinite.Realizer: Realization of the local finiteness of an indexed family of sets.
• Compact.Realizer: Realization of the compactness of a set.

structure Ctop (α : Type u_1) (σ : Type u_2) : Type (max u_1 u_2)

A Ctop α σ is a realization of a topology (basis) on α, represented by a type σ together with operations for the top element and the intersection operation.

• f : σ → Set α
• top : α → σ
• top_mem : ∀ (x : α), x ∈ self.f (self.top x)
• inter : (a b : σ) → (x : α) → x ∈ self.f a ∩ self.f b → σ
• inter_mem : ∀ (a b : σ) (x : α) (h : x ∈ self.f a ∩ self.f b), x ∈ self.f (self.inter a b x h)
• inter_sub : ∀ (a b : σ) (x : α) (h : x ∈ self.f a ∩ self.f b), self.f (self.inter a b x h) ⊆ self.f a ∩ self.f b

theorem Ctop.top_mem {α : Type u_1} {σ : Type u_2} (self : Ctop α σ) (x : α) : x ∈ self.f (self.top x)

theorem Ctop.inter_mem {α : Type u_1} {σ : Type u_2} (self : Ctop α σ) (a : σ) (b : σ) (x : α) (h : x ∈ self.f a ∩ self.f b) : x ∈ self.f (self.inter a b x h)

theorem Ctop.inter_sub {α : Type u_1} {σ : Type u_2} (self : Ctop α σ) (a : σ) (b : σ) (x : α) (h : x ∈ self.f a ∩ self.f b) : self.f (self.inter a b x h) ⊆ self.f a ∩ self.f b

instance instInhabitedCtopSet {α : Type u_1} : Inhabited (Ctop α (Set α))

Equations

• One or more equations did not get rendered due to their size.

instance Ctop.instCoeFunForallSet {α : Type u_1} {σ : Type u_3} : CoeFun (Ctop α σ) fun (x : Ctop α σ) => σ → Set α

Equations

• Ctop.instCoeFunForallSet = { coe := Ctop.f }

theorem Ctop.coe_mk {α : Type u_1} {σ : Type u_3} (f : σ → Set α) (T : α → σ) (h₁ : ∀ (x : α), x ∈ f (T x)) (I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ) (h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)) (h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b) (a : σ) : { f := f, top := T, top_mem := h₁, inter := I, inter_mem := h₂, inter_sub := h₃ }.f a = f a

def Ctop.ofEquiv {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ ≃ τ) : Ctop α σ → Ctop α τ

Map a Ctop to an equivalent representation type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ctop.ofEquiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ ≃ τ) (F : Ctop α σ) (a : τ) : (Ctop.ofEquiv E F).f a = F.f (E.symm a)

def Ctop.toTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) : TopologicalSpace α

Every Ctop is a topological space.

Equations

• F.toTopsp = TopologicalSpace.generateFrom (Set.range F.f)

theorem Ctop.toTopsp_isTopologicalBasis {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) : TopologicalSpace.IsTopologicalBasis (Set.range F.f)

@[simp]

theorem Ctop.mem_nhds_toTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) {s : Set α} {a : α} : s ∈ nhds a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s

structure Ctop.Realizer (α : Type u_6) [T : TopologicalSpace α] : Type (max (u_5 + 1) u_6)

A Ctop realizer for the topological space T is a Ctop which generates T.

• σ : Type u_5
• F : Ctop α self.σ
• eq : self.F.toTopsp = T

theorem Ctop.Realizer.eq {α : Type u_6} [T : TopologicalSpace α] (self : Ctop.Realizer α) : self.F.toTopsp = T

def Ctop.toRealizer {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) : Ctop.Realizer α

A Ctop realizes the topological space it generates.

Equations

• F.toRealizer = { σ := σ, F := F, eq := ⋯ }

instance instInhabitedRealizer {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) : Inhabited (Ctop.Realizer α)

Equations

• instInhabitedRealizer F = { default := F.toRealizer }

theorem Ctop.Realizer.is_basis {α : Type u_1} [T : TopologicalSpace α] (F : Ctop.Realizer α) : TopologicalSpace.IsTopologicalBasis (Set.range F.F.f)

theorem Ctop.Realizer.mem_nhds {α : Type u_1} [T : TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} {a : α} : s ∈ nhds a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s

theorem Ctop.Realizer.isOpen_iff {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} : IsOpen s ↔ ∀ a ∈ s, ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s

theorem Ctop.Realizer.isClosed_iff {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} : IsClosed s ↔ ∀ (a : α), (∀ (b : F.σ), a ∈ F.F.f b → ∃ (z : α), z ∈ F.F.f b ∩ s) → a ∈ s

theorem Ctop.Realizer.mem_interior_iff {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} {a : α} : a ∈ interior s ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s

theorem Ctop.Realizer.isOpen {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (s : F.σ) : IsOpen (F.F.f s)

theorem Ctop.Realizer.ext' {α : Type u_1} [T : TopologicalSpace α] {σ : Type u_5} {F : Ctop α σ} (H : ∀ (a : α) (s : Set α), s ∈ nhds a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s) : F.toTopsp = T

theorem Ctop.Realizer.ext {α : Type u_1} [T : TopologicalSpace α] {σ : Type u_5} {F : Ctop α σ} (H₁ : ∀ (a : σ), IsOpen (F.f a)) (H₂ : ∀ (a : α), ∀ s ∈ nhds a, ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s) : F.toTopsp = T

def Ctop.Realizer.id {α : Type u_1} [TopologicalSpace α] : Ctop.Realizer α

The topological space realizer made of the open sets.

Equations

• One or more equations did not get rendered due to their size.

def Ctop.Realizer.ofEquiv {α : Type u_1} {τ : Type u_4} [TopologicalSpace α] (F : Ctop.Realizer α) (E : F.σ ≃ τ) : Ctop.Realizer α

Replace the representation type of a Ctop realizer.

Equations

• F.ofEquiv E = { σ := τ, F := Ctop.ofEquiv E F.F, eq := ⋯ }

@[simp]

theorem Ctop.Realizer.ofEquiv_σ {α : Type u_1} {τ : Type u_4} [TopologicalSpace α] (F : Ctop.Realizer α) (E : F.σ ≃ τ) : (F.ofEquiv E).σ = τ

@[simp]

theorem Ctop.Realizer.ofEquiv_F {α : Type u_1} {τ : Type u_4} [TopologicalSpace α] (F : Ctop.Realizer α) (E : F.σ ≃ τ) (s : τ) : (F.ofEquiv E).F.f s = F.F.f (E.symm s)

def Ctop.Realizer.nhds {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (a : α) : (nhds a).Realizer

A realizer of the neighborhood of a point.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ctop.Realizer.nhds_σ {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (a : α) : (F.nhds a).σ = { s : F.σ // a ∈ F.F.f s }

@[simp]

theorem Ctop.Realizer.nhds_F {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (a : α) (s : (F.nhds a).σ) : (F.nhds a).F.f s = F.F.f ↑s

theorem Ctop.Realizer.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {m : β → α} {f : Filter β} (F : f.Realizer) (R : Ctop.Realizer α) {a : α} : Filter.Tendsto m f (nhds a) ↔ ∀ (t : R.σ), a ∈ R.F.f t → ∃ (s : F.σ), ∀ x ∈ F.F.f s, m x ∈ R.F.f t

structure LocallyFinite.Realizer {α : Type u_1} {β : Type u_2} [TopologicalSpace α] (F : Ctop.Realizer α) (f : β → Set α) : Type (max (max u_1 u_2) u_5)

A LocallyFinite.Realizer F f is a realization that f is locally finite, namely it is a choice of open sets from the basis of F such that they intersect only finitely many of the values of f.

• bas : (a : α) → { s : F.σ // a ∈ F.F.f s }
• sets : (x : α) → Fintype ↑{i : β | (f i ∩ F.F.f ↑(self.bas x)).Nonempty}

theorem LocallyFinite.Realizer.to_locallyFinite {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {F : Ctop.Realizer α} {f : β → Set α} (R : LocallyFinite.Realizer F f) : LocallyFinite f

theorem locallyFinite_iff_exists_realizer {α : Type u_1} {β : Type u_2} [TopologicalSpace α] (F : Ctop.Realizer α) {f : β → Set α} : LocallyFinite f ↔ Nonempty (LocallyFinite.Realizer F f)

instance instNonemptyRealizerOfFinite {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Finite β] (F : Ctop.Realizer α) (f : β → Set α) : Nonempty (LocallyFinite.Realizer F f)

Equations

• ⋯ = ⋯

def Compact.Realizer {α : Type u_1} [TopologicalSpace α] (s : Set α) : Type (max (max (max u_1 (u_5 + 1)) u_5) u_1)

A Compact.Realizer s is a realization that s is compact, namely it is a choice of finite open covers for each set family covering s.

Equations

• Compact.Realizer s = ({f : Filter α} → (F : f.Realizer) → (x : F.σ) → f ≠ ⊥ → F.F.f x ⊆ s → { a : α // a ∈ s ∧ nhds a ⊓ f ≠ ⊥ })

instance instInhabitedRealizerEmptyCollectionSet {α : Type u_1} [TopologicalSpace α] : Inhabited (Compact.Realizer ∅)

Equations

• instInhabitedRealizerEmptyCollectionSet = { default := fun {f : Filter α} (F : f.Realizer) (x : F.σ) (h : f ≠ ⊥) (hF : F.F.f x ⊆ ∅) => let_fun this := ⋯; absurd this h }