densityProcess_empty — Mathlib

English

For any kernels κ and ν and any a ∈ α, x ∈ γ, the density κ ν a x applied to the empty set is zero.

Русский

Для любых ядер κ, ν и любых a ∈ α, x ∈ γ плотность κ ν a x на пустом множестве равна нулю.

LaTeX

$$$\density κ ν a x ∅ = 0$$$

Lean4

@[simp]
theorem densityProcess_empty (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ) (a : α) (x : γ) :
    densityProcess κ ν n a x ∅ = 0 := by simp [densityProcess]

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