add_apply — Mathlib

English

Addition of outer measures is defined pointwise: for any sets s, (m1 + m2)(s) = m1(s) + m2(s).

Русский

Сумма внешних мер определяется по точкам: для любого множества s имеем (m1 + m2)(s) = m1(s) + m2(s).

LaTeX

$$$\forall m_1,m_2:\, OuterMeasure\ \alpha,\forall s:\, Set\ \alpha,\ (m_1 + m_2)\,s = m_1\,s + m_2\,s.$$$

Lean4

theorem add_apply (m₁ m₂ : OuterMeasure α) (s : Set α) : (m₁ + m₂) s = m₁ s + m₂ s :=
  rfl

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