support_gaussianPDF — Mathlib

English

For hv := v ≠ 0, Function.support (gaussianPDF μ v) = Set.univ.

Русский

Для hv := v ≠ 0, область поддержки gaussianPDF μ v равно всему ℝ (Set.univ).

LaTeX

$$$\operatorname{Function.support}(gaussianPDF\\mu \\ v) = Set.univ$$$

Lean4

@[simp]
theorem support_gaussianPDF {μ : ℝ} {v : ℝ≥0} (hv : v ≠ 0) : Function.support (gaussianPDF μ v) = Set.univ :=
  by
  ext x
  simp only [Set.mem_univ, iff_true]
  exact (gaussianPDF_pos _ hv x).ne'

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