id_prod_eq — Mathlib

English

The identity kernel on a product equals the product of deterministic fst and snd projections: id_prod_eq expresses @Kernel.id(α × β) as deterministic fst ×κ deterministic snd.

Русский

Ядро идентичности на произведение равно произведению детерминированных проекций fst и snd.

LaTeX

$$$\\displaystyle @Kernel.id (\\alpha \\times \\beta) = (\\mathrm{deterministic} \\mathrm{Prod.fst} \\; \\mathrm{measurable\_fst}) \\times_K (\\mathrm{deterministic} \\mathrm{Prod.snd} \\; \\mathrm{measurable\_snd})$$$

Lean4

theorem id_prod_eq :
    @Kernel.id (α × β) inferInstance =
      (deterministic Prod.fst measurable_fst) ×ₖ (deterministic Prod.snd measurable_snd) :=
  by
  rw [deterministic_prod_deterministic]
  rfl

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