density_fst_univ — Mathlib

English

For almost every x (with respect to fst κ a), density κ (fst κ) a x univ = 1.

Русский

Пусть почти все x по fst κ a удовлетворяют density κ (fst κ) a x univ = 1.

LaTeX

$$$\\forall^{\\mathrm{ae}} x\\;\\partial(\\mathrm{fst}\\,κ\\,a),\\; \\density κ (fst κ) a x univ = 1$$$

Lean4

theorem density_fst_univ (κ : Kernel α (γ × β)) [IsFiniteKernel κ] (a : α) :
    ∀ᵐ x ∂(fst κ a), density κ (fst κ) a x univ = 1 :=
  by
  have h := fun n ↦ densityProcess_fst_univ_ae κ n a
  rw [← ae_all_iff] at h
  filter_upwards [h] with x hx
  simp [density, hx]

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