- f : σ → set α
- top : α → σ
- top_mem : ∀ (x : α), x ∈ c.f (c.top x)
- inter : Π (a b : σ) (x : α), x ∈ c.f a ∩ c.f b → σ
- inter_mem : ∀ (a b : σ) (x : α) (h : x ∈ c.f a ∩ c.f b), x ∈ c.f (c.inter a b x h)
- inter_sub : ∀ (a b : σ) (x : α) (h : x ∈ c.f a ∩ c.f b), c.f (c.inter a b x h) ⊆ c.f a ∩ c.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.
@[instance]
@[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 := _}
@[simp]
theorem
ctop.of_equiv_val
{α : Type u_1}
{σ : Type u_3}
{τ : Type u_4}
(E : σ ≃ τ)
(F : ctop α σ)
(a : τ) :
Every ctop is a topological space.
Equations
theorem
ctop.realizer.is_open
{α : Type u_1}
[topological_space α]
(F : ctop.realizer α)
(s : F.σ) :
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 α) :
F.σ ≃ τ → ctop.realizer α
@[simp]
theorem
ctop.realizer.of_equiv_σ
{α : Type u_1}
{τ : Type u_4}
[topological_space α]
(F : ctop.realizer α)
(E : F.σ ≃ τ) :
@[simp]
theorem
ctop.realizer.of_equiv_F
{α : Type u_1}
{τ : Type u_4}
[topological_space α]
(F : ctop.realizer α)
(E : F.σ ≃ τ)
(s : τ) :
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]
theorem
ctop.realizer.nhds_σ
{α : Type u_1}
{β : Type u_2}
[topological_space α]
(m : α → β)
(F : ctop.realizer α)
(a : α) :
@[simp]
theorem
ctop.realizer.nhds_F
{α : Type u_1}
{β : Type u_2}
[topological_space α]
(m : α → β)
(F : ctop.realizer α)
(a : α)
(s : (F.nhds a).σ) :
theorem
ctop.realizer.tendsto_nhds_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{m : β → α}
{f : filter β}
(F : f.realizer)
(R : ctop.realizer α)
{a : α} :
theorem
locally_finite.realizer.to_locally_finite
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{F : ctop.realizer α}
{f : β → set α} :
theorem
locally_finite_iff_exists_realizer
{α : Type u_1}
{β : Type u_2}
[topological_space α]
(F : ctop.realizer α)
{f : β → set α} :