Theorems · Theorem · general topology

exists_seq_infinite_isOpen_pairwise_disjoint

∀ (X : Type u_1) [inst : TopologicalSpace X] [T2Space X] [Infinite X],
  ∃ U, (∀ (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.

Defined in

Mathlib.Topology.NatEmbedding

Cited by

1 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceT2SpaceInfinite