coe_iSup — Mathlib

English

If f : ι → OuterMeasure α, then the underlying function of the supremum equals the supremum of the underlying functions: for all s, (iSup i, f i)(s) = iSup i, f i(s).

Русский

Пусть f : ι → OuterMeasure α. Тогда функция, лежащая в основе наибольшего по индексу комплекса мер, равна наибольшему по индексу значению функций: для каждого s выполняется (iSup i, f i)(s) = iSup i, f i(s).

LaTeX

$$$ (\iSup_{i} f_i)(s) = \iSup_{i} f_i(s) $$$

Lean4

@[norm_cast]
theorem coe_iSup {ι} (f : ι → OuterMeasure α) : ⇑(⨆ i, f i) = ⨆ i, ⇑(f i) :=
  funext fun s => by simp

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