continuousAt_sign — Mathlib

English

If θ is an angle with θ ≠ 0 and θ ≠ π, then the sign function on angles is continuous at θ.

Русский

Пусть θ — угол, и θ ≠ 0, θ ≠ π. Тогда функция sign по углу непрерывна в точке θ.

LaTeX

$$$ (\theta \neq 0) \land (\theta \neq \pi) \Rightarrow \operatorname{ContinuousAt}(\mathrm{sign}, \theta) $$$

Lean4

theorem continuousAt_sign {θ : Angle} (h0 : θ ≠ 0) (hpi : θ ≠ π) : ContinuousAt sign θ :=
  (continuousAt_sign_of_ne_zero (sin_ne_zero_iff.2 ⟨h0, hpi⟩)).comp continuous_sin.continuousAt

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