gaussianPDFReal_sub — Mathlib

English

For μ ∈ ℝ, v ∈ ℝ≥0, x, y ∈ ℝ, gaussianPDFReal μ v (x − y) = gaussianPDFReal (μ + y) v x.

Русский

Для μ ∈ ℝ, v ∈ ℝ≥0, x, y ∈ ℝ, gaussianPDFReal μ v (x − y) = gaussianPDFReal (μ + y) v x.

LaTeX

$$$gaussianPDFReal\\mu \\ v (x - y) = gaussianPDFReal(\\mu + y) \\ v \\ x$$$

Lean4

theorem gaussianPDFReal_sub {μ : ℝ} {v : ℝ≥0} (x y : ℝ) : gaussianPDFReal μ v (x - y) = gaussianPDFReal (μ + y) v x :=
  by
  simp only [gaussianPDFReal]
  rw [sub_add_eq_sub_sub_swap]

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