innerContent_of_isCompact — Mathlib

English

The inner content of a supremum of a sequence of opens is bounded by the sum of the innerContents: μ.innerContent (iSup U_i) ≤ sum μ.innerContent(U_i).

Русский

Внутреннее содержимое верхнего предела последовательности открытых множеств ограничено суммой их внутренних содержимых.

LaTeX

$$$\mu.innerContent\bigl(\sup_i U_i\bigr) \le \sum_i \mu.innerContent(U_i)$$$

Lean4

theorem innerContent_of_isCompact {K : Set G} (h1K : IsCompact K) (h2K : IsOpen K) :
    μ.innerContent ⟨K, h2K⟩ = μ ⟨K, h1K⟩ :=
  le_antisymm (iSup₂_le fun _ hK' => μ.mono _ ⟨K, h1K⟩ hK') (μ.le_innerContent _ _ Subset.rfl)

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