rieszContentAux_le — Mathlib

English

For every compact K, the Riesz content λΛ(K) is finite: it is not equal to infinity.

Русский

Для каждого компактного множества K контент Рiesz конечен: не равен бесконечности.

LaTeX

$$$\\lambda(K) \\neq \\infty.$$$

Lean4

/-- Any compactly supported continuous nonnegative `f` such that `f ≥ 1` on `K` gives an upper bound
on the content of `K`; namely `λ(K) ≤ Λ f`. -/
theorem rieszContentAux_le {K : Compacts X} {f : C_c(X, ℝ≥0)} (h : ∀ x ∈ K, (1 : ℝ≥0) ≤ f x) :
    rieszContentAux Λ K ≤ Λ f :=
  csInf_le (OrderBot.bddBelow _) ⟨f, ⟨h, rfl⟩⟩

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