Theorems · Theorem · general topology

countable_setOfPred_isolated_right_within

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {s : Set α}, {x | x ∈ s ∧ nhdsWithin x (s ∩ Set.Ioi x) = ⊥}.Countable

The set of points in a set which are isolated on the right in this set is countable when the space is second-countable.

Defined in

Mathlib.Topology.Order.LeftRightNhds

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologySecondCountableTopology