English
If a family of pairwise disjoint intervals Ioo(x, y) indexed by s is such that x < y for all x in s, then s is countable given second countability.
Русский
Если семейство попарно несовмещённых интервалов Ioo(x,y) индексируемое множеством s, и каждый x удовлетворяет x<y, то s счётно; дано второе счетное базисное пространство.
LaTeX
$$s.Countable given h : s.PairwiseDisjoint (fun x => Ioo x (y x)) and h' : ∀ x ∈ s, x < y x$$
Lean4
/-- Consider a disjoint family of intervals `(x, y)` with `x < y` in a second-countable space.
Then the family is countable.
This is not a straightforward consequence of second-countability as some of these intervals might be
empty (but in fact this can happen only for countably many of them). -/
theorem countable_of_Ioo [OrderTopology α] [SecondCountableTopology α] {y : α → α} {s : Set α}
(h : PairwiseDisjoint s fun x => Ioo x (y x)) (h' : ∀ x ∈ s, x < y x) : s.Countable :=
have : (s \ {x | ∃ y, x ⋖ y}).Countable :=
(h.subset diff_subset).countable_of_isOpen (fun _ _ => isOpen_Ioo) fun x hx =>
(h' _ hx.1).exists_lt_lt (mt (Exists.intro (y x)) hx.2)
this.of_diff countable_setOf_covBy_right
