one_le_coe_iff

Mathlib.Data.ENNReal.Basic

URI: https://scilib.ai/kg/mathlib#ENNReal.one_le_coe_iff

English

For any r ∈ NNReal, (1 ≤ ↑r) if and only if (1 ≤ r).

Русский

Для любого r ∈ NNReal верно: 1 ≤ ↑r тогда и только если 1 ≤ r.

LaTeX

$$$$ 1 \leq (\uparrow r) \;\iff\; 1 \leq r. $$$$

Lean4

@[simp, norm_cast]
theorem one_le_coe_iff : (1 : ℝ≥0∞) ≤ ↑r ↔ 1 ≤ r :=
  coe_le_coe

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

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

Разделы

Аффилиация

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