get_prodLift — Mathlib

English

For x and h in the domain, the component extraction satisfies (f.prodLift g)(x).get h = ((f x).get h.1, (g x).get h.2).

Русский

Для x и индексов h вернётся пара значений: (f.prodLift g)(x).get h = ((f x).get h.1, (g x).get h.2).

LaTeX

$$$$ (f.prodLift g)(x).get(h) = ((f x).get(h.1), (g x).get(h.2)). $$$$

Lean4

theorem get_prodLift (f : α →. β) (g : α →. γ) (x : α) (h) : (f.prodLift g x).get h = ((f x).get h.1, (g x).get h.2) :=
  rfl

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