symm — Mathlib

English

Let f: Ω → β and g: Ω → β' be random-like maps. If f and g are conditionally independent given the conditioning structure μ, then they are conditionally independent with the roles of f and g swapped as well.

Русский

Пусть f: Ω → β и g: Ω → β' — случайные величины. Если f и g условно независимы относительно условия μ, то они условно независимы и при обмене их ролями (f и g сохраняют свой характер независимости).

LaTeX

$$$\operatorname{CondIndepFun} \; m' \; hm' \; f \; g \; μ \Rightarrow \operatorname{CondIndepFun} \; m' \; hm' \; g \; f \; μ$$$

Lean4

@[symm]
nonrec theorem symm {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {f : Ω → β} {g : Ω → β'}
    (hfg : CondIndepFun m' hm' f g μ) : CondIndepFun m' hm' g f μ :=
  hfg.symm

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