countable_of_isolated_left' — Mathlib

English

A pairwise disjoint family of open intervals Ioo(x, y) indexed by a second-countable space is countable.

Русский

Парно несовместная совокупность открытых интервалов Ioo(x,y) в второй счетной среде счетна.

LaTeX

$$There is a countable family of pairwise disjoint Ioo-intervals under second countability.$$

Lean4

/-- The set of points which are isolated on the left is countable when the space is
second-countable. -/
theorem countable_of_isolated_left' [OrderTopology α] [SecondCountableTopology α] :
    Set.Countable {x : α | ∃ y, y < x ∧ Ioo y x = ∅} := by
  simpa only [← covBy_iff_Ioo_eq] using countable_setOf_covBy_left

Похожие утверждения