sign_eq_one_iff

Mathlib.Data.Sign.Defs

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

← MathLib Explorer

English

sign a = 1 iff 0 < a.

Русский

sign(a) = 1 тогда и только тогда, когда 0 < a.

LaTeX

$$$sign(a) = 1 \iff 0 < a$$$

Lean4

theorem sign_eq_one_iff : sign a = 1 ↔ 0 < a :=
  by
  refine ⟨fun h => ?_, fun h => sign_pos h⟩
  by_contra hn
  rw [sign_apply, if_neg hn] at h
  split_ifs at h

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

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

Разделы

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

Аффилиация

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