continuousAt_sign_of_ne_zero

Mathlib.Topology.Instances.Sign

URI: https://scilib.ai/kg/mathlib#continuousAt_sign_of_ne_zero

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem continuousAt_sign_of_ne_zero {a : α} (h : a ≠ 0) : ContinuousAt SignType.sign a :=
  by
  rcases h.lt_or_gt with (h_neg | h_pos)
  · exact continuousAt_sign_of_neg h_neg
  · exact continuousAt_sign_of_pos h_pos

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru