coe_iSup — Mathlib

English

The image of the supremum of a family of NNReal corresponds to the supremum of the images.

Русский

Образ супремума семейства NNReal соответствует супремуму образов.

LaTeX

$$$ (\\uparrow) (\\mathrm{iSup}\\ i \\mapsto s i) = \\mathrm{iSup}\\ i \\mapsto (\\uparrow)(s i). $$$

Lean4

@[simp, norm_cast]
theorem coe_iSup {ι : Sort*} (s : ι → ℝ≥0) : (↑(⨆ i, s i) : ℝ) = ⨆ i, ↑(s i) := by
  rw [iSup, iSup, coe_sSup, ← Set.range_comp]; rfl

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