coe_comp_toNNReal_comp — Mathlib

English

If f: ι → ENNReal avoids ∞, then ENNReal.ofNNReal ∘ ENNReal.toNNReal ∘ f = f.

Русский

Если f: ι → ENNReal не принимает значение ∞, то ENNReal.ofNNReal ∘ ENNReal.toNNReal ∘ f = f.

LaTeX

$$$\forall f: \iota \to ENNReal\, (\forall x, f(x) \neq \infty) \Rightarrow (\mathrm{ofNNReal} \circ \mathrm{toNNReal} \circ f) = f$$$

Lean4

@[simp]
theorem coe_comp_toNNReal_comp {ι : Type*} {f : ι → ℝ≥0∞} (hf : ∀ x, f x ≠ ∞) :
    (fun (x : ℝ≥0) => (x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f = f :=
  by
  ext x
  simp [coe_toNNReal (hf x)]

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