inf — Mathlib

English

The Finite Strongly Measurable class is compatible with min and max operations.

Русский

Класс финитно сильно измеримых совместим с операциями min и max.

LaTeX

$$$\text{FinStronglyMeasurable}(f) \land \text{FinStronglyMeasurable}(g) \Rightarrow \text{FinStronglyMeasurable}(\min\{f,g\}) \land \text{FinStronglyMeasurable}(\max\{f,g\})$$$

Lean4

@[aesop safe 20 (rule_sets := [Measurable])]
protected theorem inf [SemilatticeInf β] [ContinuousInf β] (hf : FinStronglyMeasurable f μ)
    (hg : FinStronglyMeasurable g μ) : FinStronglyMeasurable (f ⊓ g) μ :=
  by
  refine
    ⟨fun n => hf.approx n ⊓ hg.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).inf_nhds (hg.tendsto_approx x)⟩
  refine (measure_mono (support_inf _ _)).trans_lt ?_
  exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩

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