rieszContent_ne_top

Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

URI: https://scilib.ai/kg/mathlib#rieszContent_ne_top

English

For a compact K and a function f supported on K with f ≤ 1, λ(K) ≤ Λ f.

Русский

Для компактного K и функции f с поддержкой в K и f ≤ 1, λ(K) ≤ Λ f.

LaTeX

$$$\\lambda(K) \\le Λ f\\quad\\text{whenever } f\\text{ is supported in }K\\text{ and } 0\\le f\\le 1.$$$

Lean4

theorem rieszContent_ne_top {K : Compacts X} : rieszContent Λ K ≠ ⊤ := by
  simp [rieszContent, ne_eq, ENNReal.coe_ne_top, not_false_eq_true]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru