continuousAt_sign_of_pos — Mathlib

English

If a > 0 in a linearly ordered topological space, 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_pos {a : α} (h : 0 < a) : ContinuousAt SignType.sign a :=
  by
  refine (continuousAt_const : ContinuousAt (fun _ => (1 : SignType)) a).congr ?_
  rw [Filter.EventuallyEq, eventually_nhds_iff]
  exact ⟨{x | 0 < x}, fun x hx => (sign_pos hx).symm, isOpen_lt' 0, h⟩

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