get_prodMap — Mathlib

English

If x = (a,b) and h is a witness that (a,b) lies in the domain of f × g, then the value is (f(a).get h.1, g(b).get h.2).

Русский

Пусть x = (a,b) и h доказывает, что (a,b) принадлежит области определения f × g. Тогда значение равно (f(a).get h.1, g(b).get h.2).

LaTeX

$$$$(f \\prodMap g)(x).get(h) = \\bigl( (f x_1).get h_1, (g x_2).get h_2 \\bigr).$$$$

Lean4

theorem get_prodMap (f : α →. γ) (g : β →. δ) (x : α × β) (h) :
    (f.prodMap g x).get h = ((f x.1).get h.1, (g x.2).get h.2) :=
  rfl

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