zero_iff_nonpos

Mathlib.Analysis.SpecialFunctions.SmoothTransition

URI: https://scilib.ai/kg/mathlib#Real.smoothTransition.zero_iff_nonpos

← MathLib Explorer

English

For every x ∈ ℝ, smoothTransition(x) = 0 holds iff x ≤ 0.

Русский

Пусть x ∈ ℝ. smoothTransition(x) = 0 тогда и только тогда, когда x ≤ 0.

LaTeX

$$$$ smoothTransition(x) = 0 \iff x \le 0. $$$$

Lean4

@[simp]
nonrec theorem zero_iff_nonpos : smoothTransition x = 0 ↔ x ≤ 0 := by
  simp only [smoothTransition, _root_.div_eq_zero_iff, (pos_denom x).ne', zero_iff_nonpos, or_false]

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

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

Разделы

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

Аффилиация

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