coe_iSup — Mathlib

English

The coercion of a pointwise supremum equals the pointwise supremum of the coerced maps.

Русский

Приведение верхнего предела по точкам даёт верхний предел по соответствующим отображениям.

LaTeX

$$$((\sup_i f_i) : \alpha \to \beta) = \sup_i (f_i).$$$

Lean4

@[simp, norm_cast]
theorem coe_iSup {ι : Sort*} [CompleteLattice β] (f : ι → α →o β) :
    ((⨆ i, f i : α →o β) : α → β) = ⨆ i, (f i : α → β) := by funext x; simp [iSup_apply]

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