# Documentation

Mathlib.Data.Analysis.Topology

# 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.

Instances For
instance instInhabitedCtopSet {α : Type u_1} :
Inhabited (Ctop α (Set α))
instance Ctop.instCoeFunCtopForAllSet {α : Type u_1} {σ : Type u_3} :
CoeFun (Ctop α σ) fun x => σSet α
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 : σ) :
Ctop.f { f := f, top := T, top_mem := h₁, inter := I, inter_mem := h₂, inter_sub := h₃ } 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.

Instances For
@[simp]
theorem Ctop.ofEquiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ τ) (F : Ctop α σ) (a : τ) :
Ctop.f () a = Ctop.f F (E.symm a)
def Ctop.toTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :

Every Ctop is a topological space.

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 Ctop.f F b Ctop.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.

Instances For
instance instInhabitedRealizerToTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :
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, a Ctop.f F.F b Ctop.f F.F b s
theorem Ctop.Realizer.isOpen_iff {α : Type u_1} [] (F : ) {s : Set α} :
∀ (a : α), a sb, a Ctop.f F.F b Ctop.f F.F b s
theorem Ctop.Realizer.isClosed_iff {α : Type u_1} [] (F : ) {s : Set α} :
∀ (a : α), (∀ (b : F), a Ctop.f F.F bz, z Ctop.f F.F b s) → a s
theorem Ctop.Realizer.mem_interior_iff {α : Type u_1} [] (F : ) {s : Set α} {a : α} :
a b, a Ctop.f F.F b Ctop.f F.F b s
theorem Ctop.Realizer.isOpen {α : Type u_1} [] (F : ) (s : F) :
IsOpen (Ctop.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 Ctop.f F b Ctop.f F b s) :
theorem Ctop.Realizer.ext {α : Type u_1} [T : ] {σ : Type u_5} {F : Ctop α σ} (H₁ : ∀ (a : σ), IsOpen (Ctop.f F a)) (H₂ : ∀ (a : α) (s : Set α), s nhds ab, a Ctop.f F b Ctop.f F b s) :
noncomputable def Ctop.Realizer.id {α : Type u_1} [] :

The topological space realizer made of the open sets.

Instances For
def Ctop.Realizer.ofEquiv {α : Type u_1} {τ : Type u_4} [] (F : ) (E : F τ) :

Replace the representation type of a Ctop realizer.

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 : τ) :
Ctop.f ().F s = Ctop.f F.F (E.symm s)
def Ctop.Realizer.nhds {α : Type u_1} [] (F : ) (a : α) :

A realizer of the neighborhood of a point.

Instances For
@[simp]
theorem Ctop.Realizer.nhds_σ {α : Type u_1} [] (F : ) (a : α) :
().σ = { s // a Ctop.f F.F s }
@[simp]
theorem Ctop.Realizer.nhds_F {α : Type u_1} [] (F : ) (a : α) (s : ().σ) :
CFilter.f ().F s = Ctop.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 Ctop.f R.F ts, ∀ (x : β), x CFilter.f F.F sm x Ctop.f R.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.

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 α) :
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.

Instances For