ofReal_pos

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.ofReal_pos

English

Order is preserved for less-than against zero: (x : K) < 0 iff x < 0 for real x.

Русский

Порядок против нуля сохраняется: (x : K) < 0 тогда и только тогда, когда x < 0 для вещественного x.

LaTeX

$$$ (x : K) < 0 \iff x < 0 $$$

Lean4

@[simp, norm_cast]
theorem ofReal_pos {x : ℝ} : 0 < (x : K) ↔ 0 < x := by rw [← ofReal_zero, ofReal_lt_ofReal]

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

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

Разделы

Аффилиация

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