English
For any compact K ⊆ X, the set of values attained by Λ on the family {f ∈ C_c(X,ℝ≥0) | ∀x∈K,1≤f(x)} is nonempty; i.e., there exists a test function f with f≥1 on K such that Λf is defined (and nontrivial).
Русский
Для любой компактной подмножества K ⊆ X множество значений Λ на семействе {f ∈ C_c(X,ℝ≥0) | ∀x∈K, 1≤f(x)} непусто; существуют тестовые функции f с f≥1 на K, для которых Λf определено.
LaTeX
$$$(\\Lambda '' \\{f: C_c(X,\\mathbb{R}_{\\ge0}) \\mid \\ \\forall x\\in K,\ \ 1\\le f(x)\\}). \\neq \\emptyset.$$$
Lean4
/-- Given a positive linear functional `Λ` on continuous compactly supported functions on `X`
with values in `ℝ≥0`, for `K ⊆ X` compact define `λ(K) = inf {Λf | 1≤f on K}`.
When `X` is a locally compact T2 space, this will be shown to be a
content, and will be shown to agree with the Riesz measure on the compact subsets `K ⊆ X`. -/
def rieszContentAux : Compacts X → ℝ≥0 := fun K => sInf (Λ '' {f : C_c(X, ℝ≥0) | ∀ x ∈ K, (1 : ℝ≥0) ≤ f x})
