add — Mathlib

English

If T and T' are dominated FinMeasAdditive, then their sum is dominated FinMeasAdditive with the sum of bounds.

Русский

Если T и T' доминированы FinMeasAdditive, то их сумма доминирована FinMeasAdditive с суммой границ.

LaTeX

$$DominatedFinMeasAdditive μ T C ∧ DominatedFinMeasAdditive μ T' C' ⇒ DominatedFinMeasAdditive μ (T+T') (C+C')$$

Lean4

theorem add (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') :
    DominatedFinMeasAdditive μ (T + T') (C + C') :=
  by
  refine ⟨hT.1.add hT'.1, fun s hs hμs => ?_⟩
  rw [Pi.add_apply, add_mul]
  exact (norm_add_le _ _).trans (add_le_add (hT.2 s hs hμs) (hT'.2 s hs hμs))

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