English
In a second countable space, a monotone function has at most countably many right-discontinuities within a set.
Русский
В пространстве второй счетности монотонная функция имеет не более счетное число правых точек разрыва на заданном множестве.
LaTeX
$$$\text{MonotoneOn } f s \rightarrow \text{Set.Countable}\{x\in s \mid \neg\text{ContinuousWithinAt}(f, s \cap Ioi x, x)\}$$$
Lean4
/-- In a second countable space, the set of points where a monotone function is not right-continuous
within a set is at most countable. Superseded by `MonotoneOn.countable_not_continuousWithinAt`
which gives the two-sided version. -/
theorem countable_not_continuousWithinAt_Ioi (hf : MonotoneOn f s) :
Set.Countable ({x ∈ s | ¬ContinuousWithinAt f (s ∩ Ioi x) x}) :=
by
apply (countable_image_lt_image_Ioi_within s f).mono
rintro x ⟨xs, hx : ¬ContinuousWithinAt f (s ∩ Ioi x) x⟩
dsimp only [mem_setOf_eq]
contrapose! hx
refine tendsto_order.2 ⟨fun m hm => ?_, fun u hu => ?_⟩
· filter_upwards [@self_mem_nhdsWithin _ _ x (s ∩ Ioi x)] with y hy
exact hm.trans_le (hf xs hy.1 (le_of_lt hy.2))
rcases hx xs u hu with ⟨v, vs, xv, fvu⟩
have : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x := by
simp [nhdsWithin_inter, mem_inf_of_left, self_mem_nhdsWithin, mem_inf_of_right, Ioo_mem_nhdsGT xv]
filter_upwards [this] with y hy
exact (hf hy.1 vs hy.2.2.le).trans_lt fvu
