sup — Mathlib

English

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

Русский

Если f и g — AEStronglyMeasurable, то их точечное наибольшее значение f ⊔ g — AEStronglyMeasurable.

LaTeX

$$$\text{AEStronglyMeasurable}(f, μ) \land \text{AEStronglyMeasurable}(g, μ) \Rightarrow \text{AEStronglyMeasurable}(f \sqcup g, μ).$$$

Lean4

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

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