mathlib3documentation

data.analysis.topology

Computational realization of topological spaces (experimental) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
• locally_finite.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 ctop
@[protected, instance]
def ctop.inhabited {α : Type u_1} :
inhabited (ctop α (set α))
Equations
@[protected, instance]
def ctop.has_coe_to_fun {α : Type u_1} {σ : Type u_3} :
has_coe_to_fun (ctop α σ) (λ (_x : ctop α σ), σ set α)
Equations
@[simp]
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₃} a = f a
def ctop.of_equiv {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ τ) :
ctop α σ ctop α τ

Map a ctop to an equivalent representation type.

Equations
@[simp]
theorem ctop.of_equiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ τ) (F : ctop α σ) (a : τ) :
F) a = F ((E.symm) a)
def ctop.to_topsp {α : Type u_1} {σ : Type u_3} (F : ctop α σ) :

Every ctop is a topological space.

Equations
theorem ctop.to_topsp_is_topological_basis {α : Type u_1} {σ : Type u_3} (F : ctop α σ) :
@[simp]
theorem ctop.mem_nhds_to_topsp {α : Type u_1} {σ : Type u_3} (F : ctop α σ) {s : set α} {a : α} :
s nhds a (b : σ), a F b F b s
structure ctop.realizer (α : Type u_5) [T : topological_space α] :
Type (max u_5 (u_6+1))

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

Instances for ctop.realizer
@[protected]
def ctop.to_realizer {α : Type u_1} {σ : Type u_3} (F : ctop α σ) :

A ctop realizes the topological space it generates.

Equations
@[protected, instance]
def ctop.realizer.inhabited {α : Type u_1} {σ : Type u_3} (F : ctop α σ) :
Equations
@[protected]
theorem ctop.realizer.is_basis {α : Type u_1} [T : topological_space α] (F : ctop.realizer α) :
@[protected]
theorem ctop.realizer.mem_nhds {α : Type u_1} [T : topological_space α] (F : ctop.realizer α) {s : set α} {a : α} :
s nhds a (b : F.σ), a (F.F) b (F.F) b s
theorem ctop.realizer.is_open_iff {α : Type u_1} (F : ctop.realizer α) {s : set α} :
(a : α), a s ( (b : F.σ), a (F.F) b (F.F) b s)
theorem ctop.realizer.is_closed_iff {α : Type u_1} (F : ctop.realizer α) {s : set α} :
(a : α), ( (b : F.σ), a (F.F) b ( (z : α), z (F.F) b s)) a s
theorem ctop.realizer.mem_interior_iff {α : Type u_1} (F : ctop.realizer α) {s : set α} {a : α} :
a (b : F.σ), a (F.F) b (F.F) b s
@[protected]
theorem ctop.realizer.is_open {α : Type u_1} (F : ctop.realizer α) (s : F.σ) :
is_open ((F.F) s)
theorem ctop.realizer.ext' {α : Type u_1} [T : topological_space α] {σ : Type u_2} {F : ctop α σ} (H : (a : α) (s : set α), s nhds a (b : σ), a F b F b s) :
theorem ctop.realizer.ext {α : Type u_1} [T : topological_space α] {σ : Type u_2} {F : ctop α σ} (H₁ : (a : σ), is_open (F a)) (H₂ : (a : α) (s : set α), s nhds a ( (b : σ), a F b F b s)) :
@[protected]
def ctop.realizer.id {α : Type u_1}  :

The topological space realizer made of the open sets.

Equations
def ctop.realizer.of_equiv {α : Type u_1} {τ : Type u_4} (F : ctop.realizer α) (E : F.σ τ) :

Replace the representation type of a ctop realizer.

Equations
@[simp]
theorem ctop.realizer.of_equiv_σ {α : Type u_1} {τ : Type u_4} (F : ctop.realizer α) (E : F.σ τ) :
(F.of_equiv E).σ = τ
@[simp]
theorem ctop.realizer.of_equiv_F {α : Type u_1} {τ : Type u_4} (F : ctop.realizer α) (E : F.σ τ) (s : τ) :
((F.of_equiv E).F) s = (F.F) ((E.symm) s)
@[protected]
def ctop.realizer.nhds {α : Type u_1} (F : ctop.realizer α) (a : α) :

A realizer of the neighborhood of a point.

Equations
@[simp]
theorem ctop.realizer.nhds_σ {α : Type u_1} (F : ctop.realizer α) (a : α) :
(F.nhds a).σ = {s // a (F.F) s}
@[simp]
theorem ctop.realizer.nhds_F {α : Type u_1} (F : ctop.realizer α) (a : α) (s : (F.nhds a).σ) :
((F.nhds a).F) s = (F.F) s.val
theorem ctop.realizer.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} {m : β α} {f : filter β} (F : f.realizer) (R : ctop.realizer α) {a : α} :
(nhds a) (t : R.σ), a (R.F) t ( (s : F.σ), (x : β), x (F.F) s m x (R.F) t)
structure locally_finite.realizer {α : Type u_1} {β : Type u_2} (F : ctop.realizer α) (f : β set α) :
Type (max u_1 u_2 u_5)

A locally_finite.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 locally_finite.realizer
theorem locally_finite.realizer.to_locally_finite {α : Type u_1} {β : Type u_2} {F : ctop.realizer α} {f : β set α} (R : f) :
theorem locally_finite_iff_exists_realizer {α : Type u_1} {β : Type u_2} (F : ctop.realizer α) {f : β set α} :
@[protected, instance]
def locally_finite.realizer.nonempty {α : Type u_1} {β : Type u_2} [finite β] (F : ctop.realizer α) (f : β set α) :
def compact.realizer {α : Type u_1} (s : set α) :
Type (max u_1 (max u_1 (u_2+1)) u_2 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 compact.realizer
@[protected, instance]
def compact.realizer.inhabited {α : Type u_1}  :
Equations