sup — Mathlib

English

If f and g are AEStronglyMeasurable, then their pointwise supremum f ⊔ g is AEStronglyMeasurable.

Русский

Если f и g являются AEStronglyMeasurable, то их точечная сумма f ⊔ g AEStronglyMeasurable.

LaTeX

$$$AEStronglyMeasurable\ f μ \rightarrow AEStronglyMeasurable\ g μ \rightarrow AEStronglyMeasurable\left(f \sqcup g\right) μ$$$

Lean4

@[fun_prop, aesop safe 20 apply (rule_sets := [Measurable])]
protected theorem sup [SemilatticeSup β] [ContinuousSup β] (hf : AEStronglyMeasurable f μ)
    (hg : AEStronglyMeasurable g μ) : AEStronglyMeasurable (f ⊔ g) μ :=
  ⟨hf.mk f ⊔ hg.mk g, hf.stronglyMeasurable_mk.sup hg.stronglyMeasurable_mk, hf.ae_eq_mk.sup hg.ae_eq_mk⟩

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