indepSet_congr

Mathlib.Probability.Independence.Kernel

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

English

The congruence principle: iIndepSet s κ μ is invariant under almost-everywhere equality of κ and η.

Русский

Принцип конгруэнтности: iIndepSet s κ μ сохраняется при почти везде равенстве κ и η.

LaTeX

$$$iIndepSet\, s\, κ\, μ \equiv iIndepSet\, s\, η\, μ$$$

Lean4

theorem indepSet_congr {s t : Set Ω} (h : κ =ᵐ[μ] η) : IndepSet s t κ μ ↔ IndepSet s t η μ :=
  indep_congr h

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

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

Разделы

Аффилиация

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