innerContent — Mathlib

English

The inner content of an open set U is the supremum of μ(K) over all compact K contained in U.

Русский

Внутреннее содержимое открытого множества U равно наивысшей (верхней) границе значений μ(K) по всем компактным K, вложенным в U.

LaTeX

$$$\mu.innerContent(U) = \sup_{K \in \mathrm{Compacts}(G),\; (K\subseteq U)} \mu(K)$$$

Lean4

/-- Constructing the inner content of a content. From a content defined on the compact sets, we
  obtain a function defined on all open sets, by taking the supremum of the content of all compact
  subsets. -/
def innerContent (U : Opens G) : ℝ≥0∞ :=
  ⨆ (K : Compacts G) (_ : (K : Set G) ⊆ U), μ K

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