def

Mathlib.Probability.Kernel.Invariance

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

English

The invariant property is defined by μ.bind κ = μ for kernels κ and measure μ.

Русский

Свойство инвариантности определяется как μ.bind κ = μ для ядра κ и меры μ.

LaTeX

$$$\\kappa\\text{ Invariant } μ \\;\\Rightarrow\\; μ.bind κ = μ$$$

Lean4

theorem «def» (hκ : Invariant κ μ) : μ.bind κ = μ :=
  hκ

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

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

Разделы

Аффилиация

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