countable_setOf_isolated_left_within

English

For any second-countable space, the set {x ∈ s | nhdsWithin x (s ∩ Iio x) = ⊥} is countable.

Русский

Во втором счетном пространстве множество {x ∈ s | nhdsWithin x (s ∩ Iio x) = ⊥} счетно.

LaTeX

$$$\{x \in s \mid \mathcal{N}_{s \cap I^{ - }(x)}(x) = \bot\} \text{ is countable }$$

Lean4

/-- The set of points in a set which are isolated on the left in this set is countable when the
space is second-countable. -/
theorem countable_setOf_isolated_left_within [SecondCountableTopology α] {s : Set α} :
    {x ∈ s | 𝓝[s ∩ Iio x] x = ⊥}.Countable :=
  countable_setOf_isolated_right_within (α := αᵒᵈ)

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