# mathlibdocumentation

topology.bases

def topological_space.is_topological_basis {α : Type u} [t : topological_space α] :
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
theorem topological_space.is_topological_basis_of_open_of_nhds {α : Type u} [t : topological_space α] {s : set (set α)} :
(∀ (u : set α), u sis_open u)(∀ (a : α) (u : set α), a u(∃ (v : set α) (H : v s), a v v u))

theorem topological_space.mem_nhds_of_is_topological_basis {α : Type u} [t : topological_space α] {a : α} {s : set α} {b : set (set α)} :
(s 𝓝 a ∃ (t : set α) (H : t b), a t t s)

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

theorem topological_space.mem_basis_subset_of_mem_open {α : Type u} [t : topological_space α] {b : set (set α)} {a : α} {u : set α} :
a u(∃ (v : set α) (H : v b), a v v u)

theorem topological_space.sUnion_basis_of_is_open {α : Type u} [t : topological_space α] {B : set (set α)} {u : set α} :
(∃ (S : set (set α)) (H : S B), u = ⋃₀S)

theorem topological_space.Union_basis_of_is_open {α : Type u} [t : topological_space α] {B : set (set α)} {u : set α} :
(∃ (β : Type u) (f : β → set α), (u = ⋃ (i : β), f i) ∀ (i : β), f i B)

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

A separable space is one with a countable dense subset, available through topological_space.exists_countable_dense. If α is also known to be nonempty, then topological_space.dense_seq provides a sequence ℕ → α with dense range, see topological_space.dense_range_dense_seq.

If α is a uniform space with countably generated uniformity filter (e.g., an emetric_space), then this condition is equivalent to topological_space.second_countable_topology α. In this case the latter should be used as a typeclass argument in theorems because Lean can automatically deduce separable_space from second_countable_topology but it can't deduce second_countable_topology and emetric_space.

Instances
theorem topological_space.exists_countable_dense (α : Type u) [t : topological_space α]  :
∃ (s : set α), s.countable

theorem topological_space.exists_dense_seq (α : Type u) [t : topological_space α] [nonempty α] :
∃ (u : → α),

A nonempty separable space admits a sequence with dense range. Instead of running cases on the conclusion of this lemma, you might want to use topological_space.dense_seq and topological_space.dense_range_dense_seq.

If α might be empty, then exists_countable_dense is the main way to use separability of α.

def topological_space.dense_seq (α : Type u) [t : topological_space α] [nonempty α] :
→ α

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

If α might be empty, then exists_countable_dense is the main way to use separability of α.

Equations
@[simp]
theorem topological_space.dense_range_dense_seq (α : Type u) [t : topological_space α] [nonempty α] :

The sequence dense_seq α has dense range.

theorem dense_range.separable_space {α : Type u_1} {β : Type u_2} {f : α → β} :

If α is a separable space and f : α → β is a continuous map with dense range, then β is a separable space as well. E.g., the completion of a separable uniform space is separable.

@[class]
structure topological_space.first_countable_topology (α : Type u) [t : topological_space α] :
Prop
• nhds_generated_countable : ∀ (a : α),

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

Instances
theorem topological_space.first_countable_topology.tendsto_subseq {α : Type u} [t : topological_space α] {u : → α} {x : α} :
(∃ (ψ : ), filter.tendsto (u ψ) filter.at_top (𝓝 x))

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

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

@[class]
structure topological_space.second_countable_topology (α : Type u) [t : topological_space α] :
Prop
• is_open_generated_countable : ∃ (b : set (set α)),

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

Instances
@[instance]

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

@[instance]

theorem topological_space.is_open_generated_countable_inter (α : Type u) [t : topological_space α]  :
∃ (b : set (set α)),

@[instance]

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

@[instance]

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

theorem topological_space.is_open_sUnion_countable {α : Type u} [t : topological_space α] (S : set (set α)) :
(∀ (s : set α), s Sis_open s)(∃ (T : set (set α)), T.countable T S ⋃₀T = ⋃₀S)