mathlib documentation

data.analysis.topology

structure ctop  :
Type u_1Type u_2Type (max u_1 u_2)
  • 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]
def ctop.has_coe_to_fun {α : Type u_1} {σ : Type u_3} :

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} :
σ τ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} :
ctop α σtopological_space α

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 𝓝 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.

def ctop.to_realizer {α : Type u_1} {σ : Type u_3} (F : ctop α σ) :

Equations
theorem ctop.realizer.mem_nhds {α : Type u_1} [T : topological_space α] (F : ctop.realizer α) {s : set α} {a : α} :
s 𝓝 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

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 α σ} :
(∀ (a : α) (s : set α), s 𝓝 a ∃ (b : σ), a F b F b s)F.to_topsp = T

theorem ctop.realizer.ext {α : Type u_1} [T : topological_space α] {σ : Type u_2} {F : ctop α σ} :
(∀ (a : σ), is_open (F a))(∀ (a : α) (s : set α), s 𝓝 a(∃ (b : σ), a F b F b s))F.to_topsp = T

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 α) :
F.σ τctop.realizer α

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)

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 (𝓝 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 α] :
ctop.realizer α(β → set α)Type (max u_1 u_2 u_5)

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 α} :

def compact.realizer {α : Type u_1} [topological_space α] :
ctop.realizer αset αType (max u_1 (max u_1 (u_3+1)) u_3 u_1)

Equations