countable_not_continuousAt — Mathlib

English

In a second countable space, the set of points where an antitone function is not continuous is at most countable.

Русский

Во втором счётном пространстве множество точек, в которых антотонная функция не непрерывна, не более счетно.

LaTeX

$$$\forall {\alpha, \beta} [LinearOrder(\alpha)] [TopologicalSpace(\alpha)] [OrderTopology(\alpha)] [LinearOrder(\beta)] [TopologicalSpace(\beta)] [OrderTopology(\beta)], (Antitone f) \rightarrow {x \mid \neg ContinuousAt f x} \text{ is countable}.$$

Lean4

/-- In a second countable space, the set of points where an antitone function is not continuous
is at most countable. -/
theorem countable_not_continuousAt (hf : Antitone f) : Set.Countable {x | ¬ContinuousAt f x} :=
  hf.dual_right.countable_not_continuousAt

Похожие утверждения