gaussianPDFReal_add — 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_add {μ : ℝ} {v : ℝ≥0} (x y : ℝ) : gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x :=
  by rw [sub_eq_add_neg, ← gaussianPDFReal_sub, sub_eq_add_neg, neg_neg]

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