ofReal_nonpos

Mathlib.Analysis.RCLike.Basic

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

English

Embedded nonpositivity is preserved: (x : K) ≤ 0 iff x ≤ 0 for real x.

Русский

Неотрицательность через ноль сохраняется: (x : K) ≤ 0 тогда и только тогда, когда x ≤ 0 для вещественного x.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem ofReal_nonpos {x : ℝ} : (x : K) ≤ 0 ↔ x ≤ 0 := by rw [← ofReal_zero, ofReal_le_ofReal]

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

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

Разделы

Аффилиация

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