mathlib documentation

data.analysis.topology

source
structure ctop (α : Type u_1) (σ : Type u_2) :
Type (max u_1 u_2)
  • 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
source
@[protected, instance]
def ctop.has_coe_to_fun {α : Type u_1} {σ : Type u_3} :
has_coe_to_fun (ctop α σ) (λ (_x : ctop α σ), σ → set α)
Equations
source
@[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
source
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
source
@[simp]
theorem ctop.of_equiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ ≃ τ) (F : ctop α σ) (a : τ) :
⇑(ctop.of_equiv E F) a = ⇑F (⇑(E.symm) a)
source
def ctop.to_topsp {α : Type u_1} {σ : Type u_3} (F : ctop α σ) :
topological_space α

Every ctop is a topological space.

Equations
source
theorem ctop.to_topsp_is_topological_basis {α : Type u_1} {σ : Type u_3} (F : ctop α σ) :
topological_space.is_topological_basis (set.range F.f)
source
@[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
source
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
  • ctop.realizer.has_sizeof_inst
source
@[protected]
def ctop.to_realizer {α : Type u_1} {σ : Type u_3} (F : ctop α σ) :
ctop.realizer α
Equations
source
@[protected]
theorem ctop.realizer.is_basis {α : Type u_1} [T : topological_space α] (F : ctop.realizer α) :
topological_space.is_topological_basis (set.range F.F.f)
source
@[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
source
theorem ctop.realizer.is_open_iff {α : Type u_1} [topological_space α] (F : ctop.realizer α) {s : set α} :
is_open s ↔ ∀ (a : α), a ∈ s → (∃ (b : F.σ), a ∈ ⇑(F.F) b ∧ ⇑(F.F) b ⊆ s)
source
theorem ctop.realizer.is_closed_iff {α : Type u_1} [topological_space α] (F : ctop.realizer α) {s : set α} :
is_closed s ↔ ∀ (a : α), (∀ (b : F.σ), a ∈ ⇑(F.F) b → (∃ (z : α), z ∈ ⇑(F.F) b ∩ s)) → a ∈ s
source
theorem ctop.realizer.mem_interior_iff {α : Type u_1} [topological_space α] (F : ctop.realizer α) {s : set α} {a : α} :
a ∈ interior s ↔ ∃ (b : F.σ), a ∈ ⇑(F.F) b ∧ ⇑(F.F) b ⊆ s
source
@[protected]
theorem ctop.realizer.is_open {α : Type u_1} [topological_space α] (F : ctop.realizer α) (s : F.σ) :
is_open (⇑(F.F) s)
source
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) :
F.to_topsp = T
source
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)) :
F.to_topsp = T
source
@[protected]
def ctop.realizer.id {α : Type u_1} [topological_space α] :
ctop.realizer α
Equations
source
def ctop.realizer.of_equiv {α : Type u_1} {τ : Type u_4} [topological_space α] (F : ctop.realizer α) (E : F.σ ≃ τ) :
ctop.realizer α
Equations
source
@[simp]
theorem ctop.realizer.of_equiv_σ {α : Type u_1} {τ : Type u_4} [topological_space α] (F : ctop.realizer α) (E : F.σ ≃ τ) :
(F.of_equiv E).σ = τ
source
@[simp]
theorem ctop.realizer.of_equiv_F {α : Type u_1} {τ : Type u_4} [topological_space α] (F : ctop.realizer α) (E : F.σ ≃ τ) (s : τ) :
⇑((F.of_equiv E).F) s = ⇑(F.F) (⇑(E.symm) s)
source
@[protected]
def ctop.realizer.nhds {α : Type u_1} [topological_space α] (F : ctop.realizer α) (a : α) :
(nhds a).realizer
Equations
source
@[simp]
theorem ctop.realizer.nhds_σ {α : Type u_1} {β : Type u_2} [topological_space α] (m : α → β) (F : ctop.realizer α) (a : α) :
(F.nhds a).σ = {s // a ∈ ⇑(F.F) s}
source
@[simp]
theorem ctop.realizer.nhds_F {α : Type u_1} {β : Type u_2} [topological_space α] (m : α → β) (F : ctop.realizer α) (a : α) (s : (F.nhds a).σ) :
⇑((F.nhds a).F) s = ⇑(F.F) s.val
source
theorem ctop.realizer.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} [topological_space α] {m : β → α} {f : filter β} (F : f.realizer) (R : ctop.realizer α) {a : α} :
filter.tendsto m f (nhds a) ↔ ∀ (t : R.σ), a ∈ ⇑(R.F) t → (∃ (s : F.σ), ∀ (x : β), x ∈ ⇑(F.F) s → m x ∈ ⇑(R.F) t)
source
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)
Instances for locally_finite.realizer
  • locally_finite.realizer.has_sizeof_inst
source
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) :
locally_finite f
source
theorem locally_finite_iff_exists_realizer {α : Type u_1} {β : Type u_2} [topological_space α] (F : ctop.realizer α) {f : β → set α} :
locally_finite f ↔ nonempty (locally_finite.realizer F f)
source
def compact.realizer {α : Type u_1} [topological_space α] (R : ctop.realizer α) (s : set α) :
Type (max u_1 (max u_1 (u_3+1)) u_3 u_1)
Equations