English
The Finite Strongly Measurable class is closed under infimum and supremum with respect to a suitable order.
Русский
Класс финитно сильно измеримых функций замкнут относительно inf и sup по подходящему порядку.
LaTeX
$$$\text{FinStronglyMeasurable}(f) \Rightarrow \text{FinStronglyMeasurable}(\min\{f,g\}) \text{ и } \text{FinStronglyMeasurable}(\max\{f,g\})$$$
Lean4
@[aesop safe 20 (rule_sets := [Measurable])]
protected theorem sup [SemilatticeSup β] [ContinuousSup β] (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).sup_nhds (hg.tendsto_approx x)⟩
refine (measure_mono (support_sup _ _)).trans_lt ?_
exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩
