add — Mathlib

English

If T and T' are FinMeasAdditive with respect to μ, then T+T' is FinMeasAdditive with respect to μ.

Русский

Если T и T' — FinMeasAdditive по отношению к μ, то T+T' — FinMeasAdditive по отношению к μ.

LaTeX

$$FinMeasAdditive μ T ∧ FinMeasAdditive μ T' ⇒ FinMeasAdditive μ (T+T')$$

Lean4

theorem add (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') : FinMeasAdditive μ (T + T') :=
  by
  intro s t hs ht hμs hμt hst
  simp only [hT s t hs ht hμs hμt hst, hT' s t hs ht hμs hμt hst, Pi.add_apply]
  abel

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