sup_disjoint — Mathlib

English

If K1 and K2 are disjoint compact sets with K1 ⊔ K2 closed, then μ(K1 ⊔ K2) = μ(K1) + μ(K2).

Русский

Если K1 и K2 — непересекающиеся компактные множества, и каждое из них замкнуто, то μ(K1 ∪ K2) = μ(K1) + μ(K2).

LaTeX

$$$\mu(K_1 \sqcup K_2) = \mu(K_1) + \mu(K_2) \quad\text{при } \mathrm{Disjoint}(K_1,K_2) \,\land\, IsClosed(K_1) \land IsClosed(K_2)$$$

Lean4

theorem sup_disjoint (K₁ K₂ : Compacts G) (h : Disjoint (K₁ : Set G) K₂) (h₁ : IsClosed (K₁ : Set G))
    (h₂ : IsClosed (K₂ : Set G)) : μ (K₁ ⊔ K₂) = μ K₁ + μ K₂ := by
  simpa [toNNReal_eq_toNNReal_iff, ← toNNReal_add] using μ.sup_disjoint' _ _ h h₁ h₂

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