mathlib docs: topology.bases

def topological_space.is_topological_basis {α : Type u} [t : topological_space α] (s : set (set α)) :

Prop

A topological basis is one that satisfies the necessary conditions so that it suffices to take unions of the basis sets to get a topology (without taking finite intersections as well).

Equations

topological_space.is_topological_basis s = ((∀ (t₁ : set α), t₁ ∈ s → ∀ (t₂ : set α), t₂ ∈ s → ∀ (x : α), x ∈ t₁ ∩ t₂ → (∃ (t₃ : set α) (H : t₃ ∈ s), x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂)) ∧ ⋃₀s = set.univ ∧ t = topological_space.generate_from s)

source

theorem topological_space.is_topological_basis_of_subbasis {α : Type u} [t : topological_space α] {s : set (set α)} (hs : t = topological_space.generate_from s) :

topological_space.is_topological_basis ((λ (f : set (set α)), ⋂₀f) '' {f : set (set α) | f.finite ∧ f ⊆ s ∧ (⋂₀f).nonempty})

source

theorem topological_space.is_topological_basis_of_open_of_nhds {α : Type u} [t : topological_space α] {s : set (set α)} (h_open : ∀ (u : set α), u ∈ s → is_open u) (h_nhds : ∀ (a : α) (u : set α), a ∈ u → is_open u → (∃ (v : set α) (H : v ∈ s), a ∈ v ∧ v ⊆ u)) :

topological_space.is_topological_basis s

source

theorem topological_space.mem_nhds_of_is_topological_basis {α : Type u} [t : topological_space α] {a : α} {s : set α} {b : set (set α)} (hb : topological_space.is_topological_basis b) :

s ∈ 𝓝 a ↔ ∃ (t : set α) (H : t ∈ b), a ∈ t ∧ t ⊆ s

source

theorem topological_space.is_open_of_is_topological_basis {α : Type u} [t : topological_space α] {s : set α} {b : set (set α)} (hb : topological_space.is_topological_basis b) (hs : s ∈ b) :

is_open s

source

theorem topological_space.mem_basis_subset_of_mem_open {α : Type u} [t : topological_space α] {b : set (set α)} (hb : topological_space.is_topological_basis b) {a : α} {u : set α} (au : a ∈ u) (ou : is_open u) :

∃ (v : set α) (H : v ∈ b), a ∈ v ∧ v ⊆ u

source

theorem topological_space.sUnion_basis_of_is_open {α : Type u} [t : topological_space α] {B : set (set α)} (hB : topological_space.is_topological_basis B) {u : set α} (ou : is_open u) :

∃ (S : set (set α)) (H : S ⊆ B), u = ⋃₀S

source

theorem topological_space.Union_basis_of_is_open {α : Type u} [t : topological_space α] {B : set (set α)} (hB : topological_space.is_topological_basis B) {u : set α} (ou : is_open u) :

∃ (β : Type u) (f : β → set α), (u = ⋃ (i : β), f i) ∧ ∀ (i : β), f i ∈ B

source

@[class]

structure topological_space.separable_space (α : Type u) [t : topological_space α] :

Prop

exists_countable_closure_eq_univ : ∃ (s : set α), s.countable ∧ closure s = set.univ

A separable space is one with a countable dense subset.

Instances

topological_space.second_countable_topology.to_separable_space

source

theorem topological_space.exists_dense_seq (α : Type u) [t : topological_space α] [topological_space.separable_space α] [nonempty α] :

∃ (u : ℕ → α), closure (set.range u) = set.univ

source

def topological_space.dense_seq (α : Type u) [t : topological_space α] [topological_space.separable_space α] [nonempty α] (a : ℕ) :

α

A sequence dense in a non-empty separable topological space.

Equations

topological_space.dense_seq α = classical.some _

source

@[simp]

theorem topological_space.dense_seq_dense (α : Type u) [t : topological_space α] [topological_space.separable_space α] [nonempty α] :

closure (set.range (topological_space.dense_seq α)) = set.univ

source

@[class]

structure topological_space.first_countable_topology (α : Type u) [t : topological_space α] :

Prop

nhds_generated_countable : ∀ (a : α), (𝓝 a).is_countably_generated

A first-countable space is one in which every point has a countable neighborhood basis.

Instances

source

theorem topological_space.first_countable_topology.tendsto_subseq {α : Type u} [t : topological_space α] [topological_space.first_countable_topology α] {u : ℕ → α} {x : α} (hx : map_cluster_pt x filter.at_top u) :

∃ (ψ : ℕ → ℕ), strict_mono ψ ∧ filter.tendsto (u ∘ ψ) filter.at_top (𝓝 x)

source

theorem topological_space.is_countably_generated_nhds {α : Type u} [t : topological_space α] [topological_space.first_countable_topology α] (x : α) :

(𝓝 x).is_countably_generated

source

theorem topological_space.is_countably_generated_nhds_within {α : Type u} [t : topological_space α] [topological_space.first_countable_topology α] (x : α) (s : set α) :

(𝓝[s] x).is_countably_generated

source

@[class]

structure topological_space.second_countable_topology (α : Type u) [t : topological_space α] :

Prop

is_open_generated_countable : ∃ (b : set (set α)), b.countable ∧ t = topological_space.generate_from b

A second-countable space is one with a countable basis.

Instances

source

@[instance]

def topological_space.second_countable_topology.to_first_countable_topology (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

topological_space.first_countable_topology α

source

theorem topological_space.second_countable_topology_induced (α : Type u) (β : Type u_1) [t : topological_space β] [topological_space.second_countable_topology β] (f : α → β) :

topological_space.second_countable_topology α

source

@[instance]

def topological_space.subtype.second_countable_topology (α : Type u) [t : topological_space α] (s : set α) [topological_space.second_countable_topology α] :

topological_space.second_countable_topology ↥s

source

theorem topological_space.is_open_generated_countable_inter (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

∃ (b : set (set α)), b.countable ∧ ∅ ∉ b ∧ topological_space.is_topological_basis b

source

@[instance]

def topological_space.topological_space.second_countable_topology (α : Type u) [t : topological_space α] {β : Type u_1} [topological_space β] [topological_space.second_countable_topology α] [topological_space.second_countable_topology β] :

topological_space.second_countable_topology (α × β)

source

@[instance]

def topological_space.second_countable_topology_fintype {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [t : Π (a : ι), topological_space («π» a)] [sc : ∀ (a : ι), topological_space.second_countable_topology («π» a)] :

topological_space.second_countable_topology (Π (a : ι), «π» a)

source

@[instance]

def topological_space.second_countable_topology.to_separable_space (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

topological_space.separable_space α

source

theorem topological_space.is_open_Union_countable {α : Type u} [t : topological_space α] [topological_space.second_countable_topology α] {ι : Type u_1} (s : ι → set α) (H : ∀ (i : ι), is_open (s i)) :

∃ (T : set ι), T.countable ∧ (⋃ (i : ι) (H : i ∈ T), s i) = ⋃ (i : ι), s i

source

theorem topological_space.is_open_sUnion_countable {α : Type u} [t : topological_space α] [topological_space.second_countable_topology α] (S : set (set α)) (H : ∀ (s : set α), s ∈ S → is_open s) :

∃ (T : set (set α)), T.countable ∧ T ⊆ S ∧ ⋃₀T = ⋃₀S