sup_le

Mathlib.MeasureTheory.Measure.Content

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Content.sup_le

English

For any two compacts K1, K2, μ(K1 ⊔ K2) ≤ μ(K1) + μ(K2).

Русский

Для любых компактных K1, K2 выполняется μ(K1 ⊔ K2) ≤ μ(K1) + μ(K2).

LaTeX

$$$\mu(K_1 \sqcup K_2) \le \mu(K_1) + \mu(K_2)$$$

Lean4

theorem sup_le (K₁ K₂ : Compacts G) : μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂ := by simpa [← toNNReal_add] using μ.sup_le' _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru