one_lt_coe_iff

Mathlib.Data.ENNReal.Basic

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

English

For p ∈ NNReal, 1 < (↑p) if and only if 1 < p.

Русский

Для p ∈ NNReal верно: 1 < ↑p тогда и только если 1 < p.

LaTeX

$$$$ 1 < (\uparrow p) \;\iff\; 1 < p. $$$$

Lean4

@[simp, norm_cast]
theorem one_lt_coe_iff : 1 < (↑p : ℝ≥0∞) ↔ 1 < p :=
  coe_lt_coe

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

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

Разделы

Аффилиация

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