indepFun_const_left — Mathlib

English

A constant random variable is independent of any other random variable.

Русский

Константная случайная величина независима от любой другой величины.

LaTeX

$$$ \\operatorname{IndepFun}(\\,c\\, , X,\\mu) $$$

Lean4

theorem indepFun_const_left {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [IsZeroOrProbabilityMeasure μ] (c : β)
    (X : Ω → β') : IndepFun (fun _ ↦ c) X μ :=
  Kernel.indepFun_const_left c X

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