English
Let f be monotone on a set s in a second countable topological space. Then the set of points x in s where f is not continuous from within s is at most countable.
Русский
Пусть f ограничено монотонной на подмножество s в пространстве с второй счётностью. Тогда множество точек x ∈ s, в которых f не непрерывна на s, конечно счётно.
LaTeX
$$$\forall {\alpha, \beta} [LinearOrder(\alpha)] [TopologicalSpace(\alpha)] [OrderTopology(\alpha)] [LinearOrder(\beta)] [TopologicalSpace(\beta)] [OrderTopology(\beta)] [SecondCountableTopology(\beta)] {s : Set(\alpha)} {f : \alpha \rightarrow \beta},\; (MonotoneOn f s) \rightarrow \{ x \in s \mid \neg ContinuousWithinAt f s x\} \text{ is countable}.$$
Lean4
/-- In a second countable space, the set of points where a monotone function is not continuous
within a set is at most countable. -/
theorem countable_not_continuousWithinAt (hf : MonotoneOn f s) : Set.Countable ({x ∈ s | ¬ContinuousWithinAt f s x}) :=
by
apply (hf.countable_not_continuousWithinAt_Ioi.union hf.countable_not_continuousWithinAt_Iio).mono
refine compl_subset_compl.1 ?_
simp only [compl_union]
rintro x ⟨hx, h'x⟩
simp only [mem_compl_iff, mem_setOf_eq, not_and, not_not] at hx h'x ⊢
intro xs
exact continuousWithinAt_iff_continuous_left'_right'.2 ⟨h'x xs, hx xs⟩
