instIsGaussianMapHSub — Mathlib

English

If μ is Gaussian and c ∈ E, then the map x ↦ x − c preserves Gaussianity: μ.map (fun x ↦ x − c) is Gaussian.

Русский

Если μ гауссова и c ∈ E, то отображение x ↦ x − c сохраняет гауссовость: μ.map (x ↦ x − c) гауссова.

LaTeX

$$$\\forall c \\in E,\\ IsGaussian(\\mu) \\Rightarrow IsGaussian(\\mu\\map (fun x \\mapsto x - c))$$$

Lean4

instance (c : E) : IsGaussian (μ.map (fun x ↦ x - c)) := by simp_rw [sub_eq_add_neg]; infer_instance

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