Infinite Hausdorff topological spaces

In this file we prove several properties of infinite Hausdorff topological spaces.

• exists_seq_infinite_isOpen_pairwise_disjoint: there exists a sequence of pairwise disjoint infinite open sets;
• exists_topology_isEmbedding_nat: there exists a topological embedding of ℕ into the space;
• exists_infinite_discreteTopology: there exists an infinite subset with discrete topology.

theorem exists_seq_infinite_isOpen_pairwise_disjoint (X : Type u_1) [TopologicalSpace X] [T2Space X] [Infinite X] : ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen (U n)) ∧ Pairwise (Function.onFun Disjoint U)

In an infinite Hausdorff topological space, there exists a sequence of pairwise disjoint infinite open sets.

theorem exists_topology_isEmbedding_nat (X : Type u_1) [TopologicalSpace X] [T2Space X] [Infinite X] : ∃ (f : ℕ → X), Topology.IsEmbedding f

If X is an infinite Hausdorff topological space, then there exists a topological embedding f : ℕ → X.

Note: this theorem is true for an infinite KC-space but the proof in that case is different.

theorem exists_infinite_discreteTopology (X : Type u_1) [TopologicalSpace X] [T2Space X] [Infinite X] : ∃ (s : Set X), s.Infinite ∧ DiscreteTopology ↑s

If X is an infinite Hausdorff topological space, then there exists an infinite set s : Set X that has the induced topology is the discrete topology.