indepFun_const_right — Mathlib

English

If X is independent of a constant-valued random variable c, then X is independent of c: IndepFun X (const c) κ μ.

Русский

Если X независим от константной величины c, то X независимa и от c: IndepFun X (константа c) κ μ.

LaTeX

$$$\IndepFun X (\text{const } c) κ μ$$$

Lean4

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

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