sup_apply — Mathlib

English

For outer measures m1 and m2, the supremum preserves evaluation: (m1 ⊔ m2)(s) = m1(s) ⊔ m2(s) for any set s.

Русский

Для внешних мер m1 и m2 верхняя сумма сохраняет оценку на каждом множестве: (m1 ⊔ m2)(s) = m1(s) ⊔ m2(s).

LaTeX

$$$ (m_1 \sqcup m_2)(s) = m_1(s) \sqcup m_2(s) $$$

Lean4

@[simp]
theorem sup_apply (m₁ m₂ : OuterMeasure α) (s : Set α) : (m₁ ⊔ m₂) s = m₁ s ⊔ m₂ s := by
  have := iSup_apply (fun b => cond b m₁ m₂) s; rwa [iSup_bool_eq, iSup_bool_eq] at this

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