range_coe_ennreal — Mathlib

English

The range of ENNReal → EReal is exactly the nonnegative portion of EReal, i.e., [0, ∞).

Русский

Множество образов ENNReal в EReal совпадает с [0, ∞).

LaTeX

$$$$ \mathrm{range}(\uparrow) = \mathrm{Ici}(0). $$$$

Lean4

@[simp]
theorem range_coe_ennreal : range ((↑) : ℝ≥0∞ → EReal) = Set.Ici 0 :=
  Subset.antisymm (range_subset_iff.2 coe_ennreal_nonneg) fun x =>
    match x with
    | ⊥ => fun h => absurd h bot_lt_zero.not_ge
    | ⊤ => fun _ => ⟨⊤, rfl⟩
    | (x : ℝ) => fun h => ⟨.some ⟨x, EReal.coe_nonneg.1 h⟩, rfl⟩

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