rieszContentAux_mono — Mathlib

English

The content λ associated to Λ is a regular content: for every compact K there exists an inner regular description and outer regular bounds consistent with Λ.

Русский

Контент λ, связанный с Λ, является регулярным: для каждого компактного K существует внутренняя и внешняя аппроксимация, согласующаяся с Λ.

LaTeX

$$$\\lambda =\\lambda_{Λ}\\ \text{ is a regular content on } X.$$$

Lean4

/-- Riesz content `λ` (associated with a positive linear functional `Λ`) is
monotone: if `K₁ ⊆ K₂` are compact subsets in `X`, then `λ(K₁) ≤ λ(K₂)`. -/
theorem rieszContentAux_mono {K₁ K₂ : Compacts X} (h : K₁ ≤ K₂) : rieszContentAux Λ K₁ ≤ rieszContentAux Λ K₂ :=
  by
  unfold rieszContentAux
  gcongr
  apply rieszContentAux_image_nonempty

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