indepFun_zero_left

Mathlib.Probability.Independence.Kernel

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

← MathLib Explorer

English

The zero-right instance for iIndepFun with general β: iIndepFun f κ 0.

Русский

Нулевой случай справа для iIndepFun с произвольным β: iIndepFun f κ 0.

LaTeX

$$$iIndepFun\, f\, κ\, 0$$$

Lean4

@[simp]
theorem indepFun_zero_left {β γ} [MeasurableSpace β] [MeasurableSpace γ] {f : Ω → β} {g : Ω → γ} :
    IndepFun f g (0 : Kernel α Ω) μ := by simp [IndepFun]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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