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.ctopthat 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.
- 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
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
- ctop.has_sizeof_inst
- ctop.inhabited
- ctop.has_coe_to_fun
@[protected, instance]
@[protected, instance]
def
ctop.has_coe_to_fun
{α : Type u_1}
{σ : Type u_3} :
has_coe_to_fun (ctop α σ) (λ (_x : ctop α σ), σ → set α)
Equations
- ctop.has_coe_to_fun = {coe := ctop.f σ}
@[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 : σ) :
Map a ctop to an equivalent representation type.
Equations
- ctop.of_equiv E {f := f, top := T, top_mem := h₁, inter := I, inter_mem := h₂, inter_sub := h₃} = {f := λ (a : τ), f (⇑(E.symm) a), top := λ (x : α), ⇑E (T x), top_mem := _, inter := λ (a b : τ) (x : α) (h : x ∈ f (⇑(E.symm) a) ∩ f (⇑(E.symm) b)), ⇑E (I (⇑(E.symm) a) (⇑(E.symm) b) x h), inter_mem := _, inter_sub := _}
Every ctop is a topological space.
Equations
A ctop realizer for the topological space T is a ctop
which generates T.
Instances for ctop.realizer
- ctop.realizer.has_sizeof_inst
- ctop.realizer.inhabited
@[protected]
A ctop realizes the topological space it generates.
@[protected, instance]
Equations
- ctop.realizer.inhabited F = {default := F.to_realizer}
@[protected]
@[protected]
theorem
ctop.realizer.is_open
{α : Type u_1}
[topological_space α]
(F : ctop.realizer α)
(s : F.σ) :
@[protected]
The topological space realizer made of the open sets.
Equations
- ctop.realizer.id = {σ := {x // is_open x}, F := {f := subtype.val (λ (x : set α), is_open x), top := λ (_x : α), ⟨set.univ α, _⟩, top_mem := _, inter := λ (_x : {x // is_open x}), ctop.realizer.id._match_2 _x, inter_mem := _, inter_sub := _}, eq := _}
- ctop.realizer.id._match_2 ⟨x, h₁⟩ = λ (_x : {x // is_open x}), ctop.realizer.id._match_1 x h₁ _x
- ctop.realizer.id._match_1 x h₁ ⟨y, h₂⟩ = λ (a : α) (h₃ : a ∈ ⟨x, h₁⟩.val ∩ ⟨y, h₂⟩.val), ⟨x ∩ y, _⟩
def
ctop.realizer.of_equiv
{α : Type u_1}
{τ : Type u_4}
[topological_space α]
(F : ctop.realizer α)
(E : F.σ ≃ τ) :
Replace the representation type of a ctop realizer.
@[simp]
theorem
ctop.realizer.of_equiv_σ
{α : Type u_1}
{τ : Type u_4}
[topological_space α]
(F : ctop.realizer α)
(E : F.σ ≃ τ) :
@[protected]
A realizer of the neighborhood of a point.
Equations
- F.nhds a = {σ := {s // a ∈ ⇑(F.F) s}, F := {f := λ (s : {s // a ∈ ⇑(F.F) s}), ⇑(F.F) s.val, pt := ⟨F.F.top a, _⟩, inf := λ (_x : {s // a ∈ ⇑(F.F) s}), ctop.realizer.nhds._match_2 F a _x, inf_le_left := _, inf_le_right := _}, eq := _}
- ctop.realizer.nhds._match_2 F a ⟨x, h₁⟩ = λ (_x : {s // a ∈ ⇑(F.F) s}), ctop.realizer.nhds._match_1 F a x h₁ _x
- ctop.realizer.nhds._match_1 F a x h₁ ⟨y, h₂⟩ = ⟨F.F.inter x y a _, _⟩
@[simp]
@[simp]
theorem
ctop.realizer.nhds_F
{α : Type u_1}
[topological_space α]
(F : ctop.realizer α)
(a : α)
(s : (F.nhds a).σ) :
structure
locally_finite.realizer
{α : Type u_1}
{β : Type u_2}
[topological_space α]
(F : ctop.realizer α)
(f : β → set α) :
Type (max u_1 u_2 u_5)
- bas : Π (a : α), {s // a ∈ ⇑(F.F) s}
- sets : Π (x : α), fintype ↥{i : β | (f i ∩ ⇑(F.F) ↑(self.bas x)).nonempty}
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
- locally_finite.realizer.has_sizeof_inst
- locally_finite.realizer.nonempty
theorem
locally_finite.realizer.to_locally_finite
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{F : ctop.realizer α}
{f : β → set α}
(R : locally_finite.realizer F f) :
theorem
locally_finite_iff_exists_realizer
{α : Type u_1}
{β : Type u_2}
[topological_space α]
(F : ctop.realizer α)
{f : β → set α} :
@[protected, instance]
def
locally_finite.realizer.nonempty
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[finite β]
(F : ctop.realizer α)
(f : β → set α) :
def
compact.realizer
{α : Type u_1}
[topological_space α]
(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]