mathlib documentation

data.analysis.topology

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
@[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 : τ) :
(ctop.of_equiv E 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
  • ctop.realizer.has_sizeof_inst
@[protected]
def ctop.to_realizer {α : Type u_1} {σ : Type u_3} (F : ctop α σ) :
Equations
@[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} [topological_space α] (F : ctop.realizer α) {s : set α} :
is_open s ∀ (a : α), a s(∃ (b : F.σ), a (F.F) b (F.F) b s)
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
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
@[protected]
theorem ctop.realizer.is_open {α : Type u_1} [topological_space α] (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} [topological_space α] :
Equations
def ctop.realizer.of_equiv {α : Type u_1} {τ : Type u_4} [topological_space α] (F : ctop.realizer α) (E : F.σ τ) :
Equations
@[simp]
theorem ctop.realizer.of_equiv_σ {α : Type u_1} {τ : Type u_4} [topological_space α] (F : ctop.realizer α) (E : F.σ τ) :
(F.of_equiv E).σ = τ
@[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)
@[protected]
def ctop.realizer.nhds {α : Type u_1} [topological_space α] (F : ctop.realizer α) (a : α) :
Equations
@[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}
@[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
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) sm x (R.F) t)
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
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 α} :
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