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