English
For any set s in a second-countable space, the set of points x in s for which the neighborhood within s intersected with (x, ∞) is empty is countable.
Русский
Для множества s в пространстве второй счетности множество точек x из s, для которых окрестность внутри s пересеченная с интервалом (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 right in this set is countable when the
space is second-countable. -/
theorem countable_setOf_isolated_right_within [SecondCountableTopology α] {s : Set α} :
{x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥}.Countable := by
/- This does not follow from `countable_setOf_isolated_right`, which gives the result when `s`
is the whole space, as one cannot use it inside the subspace since it doesn't have the order
topology. Instead, we follow the main steps of its proof. -/
let t := {x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
suffices H : t.Countable
by
have : {x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x | IsTop x} :=
by
intro x hx
by_cases h'x : IsTop x
· simp [h'x]
· simpa [-sep_and, t, h'x]
apply Countable.mono this
simp [H, (subsingleton_isTop α).countable]
have (x) (hx : x ∈ t) : ∃ y > x, s ∩ Ioo x y = ∅ :=
by
simp only [← empty_mem_iff_bot, mem_nhdsWithin_iff_exists_mem_nhds_inter, subset_empty_iff, IsTop, not_forall,
not_le, mem_setOf_eq, t] at hx
rcases hx.2.1 with ⟨u, hu, h'u⟩
obtain ⟨y, hxy, hy⟩ : ∃ y, x < y ∧ Ico x y ⊆ u := exists_Ico_subset_of_mem_nhds hu hx.2.2
refine ⟨y, hxy, ?_⟩
contrapose! h'u
apply h'u.mono
intro z hz
exact ⟨hy ⟨hz.2.1.le, hz.2.2⟩, hz.1, hz.2.1⟩
choose! y hy h'y using this
apply Set.PairwiseDisjoint.countable_of_Ioo (y := y) _ hy
simp only [PairwiseDisjoint, Set.Pairwise, Function.onFun]
intro a ha b hb hab
wlog H : a < b generalizing a b with h
· have : b < a := lt_of_le_of_ne (not_lt.1 H) hab.symm
exact (h hb ha hab.symm this).symm
have : y a ≤ b := by
by_contra!
have : b ∈ s ∩ Ioo a (y a) := by simp [hb.1, H, this]
simp [h'y a ha] at this
rw [disjoint_iff_forall_ne]
exact fun u hu v hv ↦ ((hu.2.trans_le this).trans hv.1).ne
