map_sInf_of_continuousAt — Mathlib

English

For an antitone function on a set s, in a second countable space, the set {x ∈ s | ¬ ContinuousWithinAt f s x} is countable.

Русский

Для антитонной функции на s во втором счётном пространстве множество {x ∈ s | ¬ ContinuousWithinAt f s x} счётно.

LaTeX

$$$\forall {s} (hf : AntitoneOn f s), Set.Countable({x ∈ s | ¬ ContinuousWithinAt f s x})$$$

Lean4

/-- A monotone function `f` sending `top` to `top` and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set. -/
theorem map_sInf_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Mf : Monotone f)
    (ftop : f ⊤ = ⊤) : f (sInf s) = sInf (f '' s) :=
  Monotone.map_sSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop

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