coe_add — Mathlib

English

The coercion to functions is additive with respect to outer measure addition: the underlying function of m1 + m2 is the sum of the underlying functions.

Русский

Переход к функциям сохраняет сложение: функция, лежащая в основе m1 + m2, равна сумме функций, лежащих в основе m1 и m2.

LaTeX

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

Lean4

@[simp]
theorem coe_add (m₁ m₂ : OuterMeasure α) : ⇑(m₁ + m₂) = m₁ + m₂ :=
  rfl

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