coe_pos

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.coe_pos

English

For r ∈ ℝ≥0, (0 : ℝ) < r is equivalent to 0 < r in NNReal.

Русский

Для r ∈ ℝ≥0: 0 < r в ℝ ⇔ 0 < r в NNReal.

LaTeX

$$$0 < r^{\uparrow} \;\Leftrightarrow\; 0 < r$$$

Lean4

@[simp, norm_cast]
theorem coe_pos : (0 : ℝ) < r ↔ 0 < r :=
  Iff.rfl

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

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

Разделы

Аффилиация

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