prodLift_fst_comp_snd_comp — Mathlib

English

The product lift of f ∘ fst and g ∘ snd equals the product map f × g.

Русский

Покрытие произведения: prodLift (f ∘ fst) (g ∘ snd) совпадает с f × g.

LaTeX

$$$$ \\operatorname{prodLift}(f \\circ \\mathrm{fst},\, g \\circ \\mathrm{snd}) = f \\prodMap g. $$$$

Lean4

@[simp]
theorem prodLift_fst_comp_snd_comp (f : α →. γ) (g : β →. δ) :
    prodLift (f.comp ((Prod.fst : α × β → α) : α × β →. α)) (g.comp ((Prod.snd : α × β → β) : α × β →. β)) =
      prodMap f g :=
  by aesop

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