inf — Mathlib

English

Let f and g be AEFinStronglyMeasurable with respect to μ. Then their pointwise infimum is AEFinStronglyMeasurable with respect to μ.

Русский

Пусть f и g являются AEFinStronglyMeasurable по отношению к μ. Тогда их точечный инфимум f ⊓ g является AEFinStronglyMeasurable по отношению к μ.

LaTeX

$$$\\text{AEFinStronglyMeasurable}_\\mu(f) \\land \\text{AEFinStronglyMeasurable}_\\mu(g) \\Rightarrow \\text{AEFinStronglyMeasurable}_\\mu(f \\wedge g)$$$

Lean4

@[aesop safe 20 (rule_sets := [Measurable])]
protected theorem inf [SemilatticeInf β] [ContinuousInf β] (hf : AEFinStronglyMeasurable f μ)
    (hg : AEFinStronglyMeasurable g μ) : AEFinStronglyMeasurable (f ⊓ g) μ :=
  ⟨hf.mk f ⊓ hg.mk g, hf.finStronglyMeasurable_mk.inf hg.finStronglyMeasurable_mk, hf.ae_eq_mk.inf hg.ae_eq_mk⟩

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