inf — Mathlib

English

If f and g are AEStronglyMeasurable, then their pointwise infimum f ⊓ g is AEStronglyMeasurable.

Русский

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

LaTeX

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

Lean4

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

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