ofReal_lt_coe_iff — Mathlib

English

Let a be a real number with a ≥ 0 and b a nonnegative real (as an element of ENNReal). Then embedding a into ENNReal via ofReal preserves strict order: ENNReal.ofReal(a) < b if and only if a < b (interpreted in real terms).

Русский

Пусть a ∈ ℝ с a ≥ 0 и b ∈ ℝ≥0 (как элемент ENNReal). Тогда включение a в ENNReal через ofReal сохраняет строгий порядок: ENNReal.ofReal(a) < b эквивалентно a < b (в действительных числах).

LaTeX

$$$0 \le a \Rightarrow \operatorname{ofReal}(a) < b \iff a < b$$$

Lean4

theorem ofReal_lt_coe_iff {a : ℝ} {b : ℝ≥0} (ha : 0 ≤ a) : ENNReal.ofReal a < b ↔ a < b :=
  (ofReal_lt_iff_lt_toReal ha coe_ne_top).trans <| by rw [coe_toReal]

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