gaussianPDF_ne_top

Mathlib.Probability.Distributions.Gaussian.Real

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.gaussianPDF_ne_top

English

For all μ ∈ ℝ, v ∈ ℝ≥0, x ∈ ℝ, gaussianPDF μ v x ≠ ∞.

Русский

Для всех μ ∈ ℝ, v ∈ ℝ≥0, x ∈ ℝ, gaussianPDF μ v x ≠ ∞.

LaTeX

$$$gaussianPDF\\mu \\ v \\ x \neq \infty$$$

Lean4

theorem gaussianPDF_ne_top {μ : ℝ} {v : ℝ≥0} {x : ℝ} : gaussianPDF μ v x ≠ ∞ := by simp [gaussianPDF]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru