withDensity_one'

Mathlib.Probability.Kernel.WithDensity

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

English

A simplification stating withDensity κ (fun _ _ => 1) equals κ.

Русский

Упрощение: withDensity κ (fun _ _ => 1) равно κ.

LaTeX

$$Kernel.withDensity κ (fun _ _ => 1) = κ$$

Lean4

@[simp]
theorem withDensity_one' (κ : Kernel α β) [IsSFiniteKernel κ] : Kernel.withDensity κ (fun _ _ ↦ 1) = κ :=
  Kernel.withDensity_one _

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

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

Разделы

Аффилиация

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