innerContent_le — Mathlib

English

If K is a compact subset with K open as a subset, then the inner content of the open representation equals the content of the compact representation: μ.innerContent ⟨K, open⟩ = μ ⟨K, compact⟩.

Русский

Если K компактно и открыто в поднаборе, тогда внутреннее содержимое открытого представления равно содержанию компактного представления: μ.innerContent ⟨K, open⟩ = μ ⟨K, compact⟩.

LaTeX

$$$\mu.innerContent ⟨K, h_2K⟩ = μ ⟨K, h_1K⟩$ при $h_1K$ компактно и $h_2K$ открыто.$$

Lean4

theorem innerContent_le (U : Opens G) (K : Compacts G) (h2 : (U : Set G) ⊆ K) : μ.innerContent U ≤ μ K :=
  iSup₂_le fun _ hK' => μ.mono _ _ (Subset.trans hK' h2)

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