countable_setOf_isolated_left — Mathlib

English

In any second-countable topological space with a linear order and order topology, the set of points x such that the left-neighborhood of x is empty is countable.

Русский

Во второй счетности топологического пространства с линейным порядком и топологией порядка множество точек x, для которых левое окрестность x пустая, счетно.

LaTeX

$$$\{x \in \alpha \mid \mathcal{N}_{(-\infty, x)}(x) = \bot\\} \text{ is countable }$$

Lean4

/-- The set of points which are isolated on the left is countable when the space is
second-countable. -/
theorem countable_setOf_isolated_left [SecondCountableTopology α] : {x : α | 𝓝[<] x = ⊥}.Countable :=
  countable_setOf_isolated_right (α := αᵒᵈ)

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