fst_prodMkRight — Mathlib

English

Let κ be a kernel from α to β × γ and δ a Type with a measurable structure. Then the first projection of the right-augmented kernel equals the right-augmented kernel of the first projection: fst(prodMkRight δ κ) = prodMkRight δ (fst κ).

Русский

Пусть κ — ядро из α в β × γ, а δ — произвольное множество с меруемой структурой. Тогда первая проекция правой надстройки ядра равна надстройке правой проекции ядра: fst(prodMkRight δ κ) = prodMkRight δ (fst κ).

LaTeX

$$$\\mathrm{fst}(\\mathrm{prodMkRight}(\\delta, \\kappa)) = \\mathrm{prodMkRight}(\\delta, \\mathrm{fst}(\\kappa))$$$

Lean4

theorem fst_prodMkRight (κ : Kernel α (β × γ)) (δ : Type*) [MeasurableSpace δ] :
    fst (prodMkRight δ κ) = prodMkRight δ (fst κ) :=
  rfl

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