natCast_lt_iff

Mathlib.Data.EReal.Basic

URI: https://scilib.ai/kg/mathlib#EReal.natCast_lt_iff

← MathLib Explorer

English

For naturals m,n, (m : EReal) < (n : EReal) iff m < n.

Русский

Для натуральных m,n: (m : EReal) < (n : EReal) тогда и только тогда, когда m < n.

LaTeX

$$$ (m : \mathrm{EReal}) < (n : \mathrm{EReal}) \iff m < n $$$

Lean4

@[norm_cast]
theorem natCast_lt_iff {m n : ℕ} : (m : EReal) < (n : EReal) ↔ m < n := by
  rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_lt_coe_iff, Nat.cast_lt]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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