prodLift_apply — Mathlib

English

The value of f.prodLift g at x equals the pair comprised of the values of f(x) and g(x) whenever both are defined.

Русский

Значение f.prodLift g в точке x равно пару значений f(x) и g(x) если оба определены.

LaTeX

$$$$ f.prodLift g x = \langle (f x).Dom \land (g x).Dom, \; (f x).get, (g x).get \rangle. $$$$

Lean4

@[simp]
theorem prodLift_apply (f : α →. β) (g : α →. γ) (x : α) :
    f.prodLift g x = ⟨(f x).Dom ∧ (g x).Dom, fun h => ((f x).get h.1, (g x).get h.2)⟩ :=
  rfl

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