toReal_gaussianPDF — Mathlib

English

For μ ∈ ℝ, v ∈ ℝ≥0, x ∈ ℝ, (gaussianPDF μ v x).toReal = gaussianPDFReal μ v x.

Русский

Для μ ∈ ℝ, v ∈ ℝ≥0, x ∈ ℝ, (gaussianPDF μ v x).toReal = gaussianPDFReal μ v x.

LaTeX

$$(gaussianPDF\\mu \\ v \\ x).toReal = gaussianPDFReal\\mu \\ v \\ x$$

Lean4

@[simp]
theorem toReal_gaussianPDF {μ : ℝ} {v : ℝ≥0} (x : ℝ) : (gaussianPDF μ v x).toReal = gaussianPDFReal μ v x := by
  rw [gaussianPDF, ENNReal.toReal_ofReal (gaussianPDFReal_nonneg μ v x)]

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