rieszContent — Mathlib

English

For every compact K, rieszContent Λ K is finite, i.e., not equal to infinity.

Русский

Для каждого компактного K контент rieszContent Λ K конечен, не равен бесконечности.

LaTeX

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

Lean4

/-- The content induced by the linear functional `Λ`. -/
noncomputable def rieszContent (Λ : C_c(X, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) : Content X
    where
  toFun := rieszContentAux Λ
  mono' := fun _ _ ↦ rieszContentAux_mono Λ
  sup_disjoint' := fun _ _ disj _ _ ↦ rieszContentAux_union Λ disj
  sup_le' := rieszContentAux_sup_le Λ

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