condIndepFun_const_left — Mathlib

English

A constant function is independent from any other random variable X under the same conditioning structure.

Русский

Константная функция независима от любой другой случайной величины X при той же условности.

LaTeX

$$$\operatorname{CondIndepFun} \; m' \; hm' \; (\lambda \_ : Ω \to β) \; X \; μ$$$

Lean4

theorem condIndepFun_const_left {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} (c : β) (X : Ω → β') :
    CondIndepFun m' hm' (fun _ ↦ c) X μ :=
  Kernel.indepFun_const_left c X

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