condDistrib_congr_right

Mathlib.Probability.Kernel.CondDistrib

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

Lean4

theorem condDistrib_congr_right {X' : α → β} (hX : X =ᵐ[μ] X') : condDistrib Y X μ = condDistrib Y X' μ :=
  condDistrib_congr (by rfl) hX

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

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

Разделы

Аффилиация

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