indepFun_const_left — Mathlib

English

If κ is a zero- or Markov-type kernel, and c is a constant, then the constant random variable maps to independence with any other variable X: IndepFun (const c) X κ μ.

Русский

Если ядро κ является нулевым или Марковским и константа c фиксирована, то константная случайная величина независима от любой другой переменной X: IndepFun (константа c) X κ μ.

LaTeX

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

Lean4

theorem indepFun_const_left {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [IsZeroOrMarkovKernel κ] (c : β')
    (X : Ω → β) : IndepFun (fun _ ↦ c) X κ μ :=
  by
  rw [IndepFun, MeasurableSpace.comap_const]
  exact indep_bot_left _

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