coe_iSup — Mathlib

English

The coercion of the supremum equals the supremum taken in WithTop α for a bounded-above family.

Русский

Приведение к WithTop сохраняет супремум: ↑(⨆ i, f i) = ⨆ i, f i в WithTop(α).

LaTeX

$$$\uparrow\left(\sup_i f(i)\right) = \sup_i f(i)\quad\text{in } WithTop(\alpha)$$$

Lean4

@[norm_cast]
theorem coe_iSup [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) : ↑(⨆ i, f i) = (⨆ i, f i : WithTop α) := by
  rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]

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