measure_le_bound

Mathlib.Probability.Kernel.Defs

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.measure_le_bound

← MathLib Explorer

English

For any a and s, κ a s ≤ κ.bound.

Русский

Для любых a и s, κ a s ≤ κ.bound.

LaTeX

$$$\kappa a s \leq \kappa.bound$$$

Lean4

theorem measure_le_bound (κ : Kernel α β) (a : α) (s : Set β) : κ a s ≤ κ.bound :=
  (measure_mono (Set.subset_univ s)).trans <| le_iSup (f := fun a ↦ κ a .univ) a

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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