coe_lt_natCast

Mathlib.Data.ENNReal.Basic

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

English

For any r ∈ NNReal and n ∈ Nat, (r : ENNReal) < n iff r < n.

Русский

Для любых r ∈ NNReal и n ∈ Nat, (r : ENNReal) < n эквивалентно r < n.

LaTeX

$$$ \forall {r : \mathbb{R}_{\\ge 0}}, {n : \mathbb{N}}, (r : \\mathbb{R}_{\\ge 0}^\\infty) < n \\iff r < n $$$

Lean4

theorem coe_lt_natCast {n : ℕ} : (r : ℝ≥0∞) < n ↔ r < n :=
  ENNReal.coe_natCast n ▸ coe_lt_coe

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

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

Разделы

Аффилиация

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