natCast_lt_coe

Mathlib.Data.ENNReal.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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