English
For an antitone function restricted to a set s, the set of points inside s where it is not continuous within s is countable in a second countable space.
Русский
Для антитонной функции, ограниченной на множество s, множество точек внутри s, где функция не непрерывна относительно s, счётно в пространстве с второй счётностью.
LaTeX
$$$\forall {\alpha, \beta} [LinearOrder(\alpha)] [TopologicalSpace(\alpha)] [OrderTopology(\alpha)] [LinearOrder(\beta)] [TopologicalSpace(\beta)] [OrderTopology(\beta)] {s : Set(\alpha)} {f : \alpha \rightarrow \beta}, (AntitoneOn f s) \rightarrow {x \in s | \neg ContinuousWithinAt f s x} \text{ is countable}.$$
Lean4
/-- In a second countable space, the set of points where an antitone function is not continuous
within a set is at most countable. -/
theorem _root_.AntitoneOn.countable_not_continuousWithinAt {s : Set α} (hf : AntitoneOn f s) :
Set.Countable ({x ∈ s | ¬ContinuousWithinAt f s x}) :=
hf.dual_right.countable_not_continuousWithinAt
