continuousAt_sign_of_neg — Mathlib

English

If a < 0, the sign function is continuous at a.

Русский

Если a < 0, знак функции непрерывен в точке a.

LaTeX

$$$ a<0 \\Rightarrow \\mathrm{ContinuousAt}(\\mathrm{SignType.sign},a). $$$

Lean4

theorem continuousAt_sign_of_neg {a : α} (h : a < 0) : ContinuousAt SignType.sign a :=
  by
  refine (continuousAt_const : ContinuousAt (fun x => (-1 : SignType)) a).congr ?_
  rw [Filter.EventuallyEq, eventually_nhds_iff]
  exact ⟨{x | x < 0}, fun x hx => (sign_neg hx).symm, isOpen_gt' 0, h⟩

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