coeFn_sup — Mathlib

English

The coeFn_sup lemma asserts that the representative of the supremum of two μ-ae equivalence classes agrees a.e. with the pointwise supremum of the representatives.

Русский

Лемма coeFn_sup утверждает, что представление верхней границы двух ae-эквивалентностей совпадает почти всюду с точечным взятием верхней границы представлений.

LaTeX

$$$(f \sqcup g).cast x =^\mathrm{ae}_{μ} f.cast x \sqcup g.cast x$ for each x in the underlying space.$$

Lean4

theorem coeFn_sup (f g : α →ₘ[μ] β) : ⇑(f ⊔ g) =ᵐ[μ] fun x => f x ⊔ g x :=
  coeFn_comp₂ _ _ _ _

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