condVar_congr_ae — Mathlib

English

If X =_μae Y, then Var[X; μ | m] =_μ Var[Y; μ | m].

Русский

Если X эквивалентна Y по μ-а-единостям, то Var[X; μ | m] эквивалентна Var[Y; μ | m].

LaTeX

$$$ X =_\mu a.e. Y \Rightarrow Var[X; μ | m] =_\mu a.e. Var[Y; μ | m] $$$

Lean4

theorem condVar_congr_ae (h : X =ᵐ[μ] Y) : Var[X; μ | m] =ᵐ[μ] Var[Y; μ | m] :=
  condExp_congr_ae <| by filter_upwards [h, condExp_congr_ae h] with ω hω hω'; dsimp; rw [hω, hω']

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