condDistrib_congr_left

Mathlib.Probability.Kernel.CondDistrib

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.condDistrib_congr_left

Lean4

theorem condDistrib_congr_left {Y' : α → Ω} (hY : Y =ᵐ[μ] Y') : condDistrib Y X μ = condDistrib Y' X μ :=
  condDistrib_congr hY (by rfl)

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

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

Разделы

Аффилиация

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