countable_setOf_covBy_left — Mathlib

English

The set of points isolated on the left is countable under OrderTopology α and SecondCountableTopology α.

Русский

Множество точек, изолированных слева, счётно при OrderTopology и SecondCountableTopology.

LaTeX

$$Set.Countable {x ∈ α | ∃ y, y ⋖ x}$$

Lean4

/-- The set of points which are isolated on the left is countable when the space is
second-countable. -/
theorem countable_setOf_covBy_left [OrderTopology α] [SecondCountableTopology α] : Set.Countable {x : α | ∃ y, y ⋖ x} :=
  by
  convert countable_setOf_covBy_right (α := αᵒᵈ) using 5
  exact toDual_covBy_toDual_iff.symm

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