English
In a second-countable OrderTopology α, the set of points x for which there exists y with x ⋖ y is countable.
Русский
В второй счетной топологии порядка α множество точек x, таких что существует y с x⋖y, счётно.
LaTeX
$${x ∈ α | ∃ y, x ⋖ y} является счётным$$
Lean4
/-- The set of points which are isolated on the right is countable when the space is
second-countable. -/
theorem countable_setOf_covBy_right [OrderTopology α] [SecondCountableTopology α] :
Set.Countable {x : α | ∃ y, x ⋖ y} := by
nontriviality α
let s := {x : α | ∃ y, x ⋖ y}
have : ∀ x ∈ s, ∃ y, x ⋖ y := fun x => id
choose! y hy using this
have Hy : ∀ x z, x ∈ s → z < y x → z ≤ x := fun x z hx => (hy x hx).le_of_lt
suffices H : ∀ a : Set α, IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
by
have : s ⊆ ⋃ a ∈ countableBasis α, {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a} := fun x hx =>
by
rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩
refine Set.Countable.mono this ?_
refine Countable.biUnion (countable_countableBasis α) fun a ha => H _ ?_
exact isOpen_of_mem_countableBasis ha
intro a ha
suffices H : Set.Countable {x | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x} from H.of_diff (subsingleton_isBot α).countable
simp only [and_assoc]
let t := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
have : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a := by
intro x hx
apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)
simpa only [IsBot, not_forall, not_le] using hx.right.right.right
choose! z hz h'z using this
have : PairwiseDisjoint t fun x => Ioc (z x) x := fun x xt x' x't hxx' =>
by
rcases hxx'.lt_or_gt with (h' | h')
· refine disjoint_left.2 fun u ux ux' => xt.2.2.1 ?_
refine h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), ?_⟩
by_contra! H
exact lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')
· refine disjoint_left.2 fun u ux ux' => x't.2.2.1 ?_
refine h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), ?_⟩
by_contra! H
exact lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')
refine this.countable_of_isOpen (fun x hx => ?_) fun x hx => ⟨x, hz x hx, le_rfl⟩
suffices H : Ioc (z x) x = Ioo (z x) (y x) by
rw [H]
exact isOpen_Ioo
exact Subset.antisymm (Ioc_subset_Ioo_right (hy x hx.1).lt) fun u hu => ⟨hu.1, Hy _ _ hx.1 hu.2⟩
