# 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
Instances For
instance instInhabitedCtopSet {α : Type u_1} :
Inhabited (Ctop α (Set α))
Equations
• One or more equations did not get rendered due to their size.
instance Ctop.instCoeFunCtopForAllSet {α : Type u_1} {σ : Type u_3} :
CoeFun (Ctop α σ) fun (x : Ctop α σ) => σSet α
Equations
• Ctop.instCoeFunCtopForAllSet = { 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.
Instances For
@[simp]
theorem Ctop.ofEquiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ τ) (F : Ctop α σ) (a : τ) :
().f a = F.f (E.symm a)
def Ctop.toTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :

Every Ctop is a topological space.

Equations
Instances For
theorem Ctop.toTopsp_isTopologicalBasis {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :
@[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 : ] :
Type (max (u_5 + 1) u_6)

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

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

A Ctop realizes the topological space it generates.

Equations
• = { σ := σ, F := F, eq := }
Instances For
instance instInhabitedRealizerToTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :
Equations
• = { default := }
theorem Ctop.Realizer.is_basis {α : Type u_1} [T : ] (F : ) :
theorem Ctop.Realizer.mem_nhds {α : Type u_1} [T : ] (F : ) {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} [] (F : ) {s : Set α} :
as, ∃ (b : F), a F.F.f b F.F.f b s
theorem Ctop.Realizer.isClosed_iff {α : Type u_1} [] (F : ) {s : Set α} :
∀ (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} [] (F : ) {s : Set α} {a : α} :
a ∃ (b : F), a F.F.f b F.F.f b s
theorem Ctop.Realizer.isOpen {α : Type u_1} [] (F : ) (s : F) :
IsOpen (F.F.f s)
theorem Ctop.Realizer.ext' {α : Type u_1} [T : ] {σ : Type u_5} {F : Ctop α σ} (H : ∀ (a : α) (s : Set α), s nhds a ∃ (b : σ), a F.f b F.f b s) :
theorem Ctop.Realizer.ext {α : Type u_1} [T : ] {σ : Type u_5} {F : Ctop α σ} (H₁ : ∀ (a : σ), IsOpen (F.f a)) (H₂ : ∀ (a : α), snhds a, ∃ (b : σ), a F.f b F.f b s) :
noncomputable def Ctop.Realizer.id {α : Type u_1} [] :

The topological space realizer made of the open sets.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Ctop.Realizer.ofEquiv {α : Type u_1} {τ : Type u_4} [] (F : ) (E : F τ) :

Replace the representation type of a Ctop realizer.

Equations
Instances For
@[simp]
theorem Ctop.Realizer.ofEquiv_σ {α : Type u_1} {τ : Type u_4} [] (F : ) (E : F τ) :
() = τ
@[simp]
theorem Ctop.Realizer.ofEquiv_F {α : Type u_1} {τ : Type u_4} [] (F : ) (E : F τ) (s : τ) :
().F.f s = F.F.f (E.symm s)
def Ctop.Realizer.nhds {α : Type u_1} [] (F : ) (a : α) :

A realizer of the neighborhood of a point.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Ctop.Realizer.nhds_σ {α : Type u_1} [] (F : ) (a : α) :
() = { s : F // a F.F.f s }
@[simp]
theorem Ctop.Realizer.nhds_F {α : Type u_1} [] (F : ) (a : α) (s : ()) :
().F.f s = F.F.f s
theorem Ctop.Realizer.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} [] {m : βα} {f : } (F : ) (R : ) {a : α} :
Filter.Tendsto m f (nhds a) ∀ (t : R), a R.F.f t∃ (s : F), xF.F.f s, m x R.F.f t
structure LocallyFinite.Realizer {α : Type u_1} {β : Type u_2} [] (F : ) (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 : β | Set.Nonempty (f i F.F.f (self.bas x))}
Instances For
theorem LocallyFinite.Realizer.to_locallyFinite {α : Type u_1} {β : Type u_2} [] {F : } {f : βSet α} (R : ) :
theorem locallyFinite_iff_exists_realizer {α : Type u_1} {β : Type u_2} [] (F : ) {f : βSet α} :
instance instNonemptyRealizer {α : Type u_1} {β : Type u_2} [] [] (F : ) (f : βSet α) :
Equations
• =
def Compact.Realizer {α : Type u_1} [] (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
Instances For
Equations
• One or more equations did not get rendered due to their size.