condIndepFun_const_right — Mathlib

English

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

Русский

Случайная величина X независима от константной функции c при той же условности.

LaTeX

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

Lean4

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

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