English
Define the product lift of two partial functions f: α →. β and g: α →. γ by (f.prodLift g)(x) = ⟨ Dom(f(x)) ∧ Dom(g(x)), a pair of gets ⟩, i.e., the product partial function sending x to a pair of values whenever both are defined.
Русский
Определим произведение частичных функций f и g как f.prodLift g, где (f.prodLift g)(x) даёт пару значений, если обе функции определены в x.
LaTeX
$$$$ (f.prodLift g)(x) = \langle (f(x)).Dom \land (g(x)).Dom, \ \big((f(x)).get, (g(x)).get\big) \rangle. $$$$
Lean4
/-- Product of partial functions. -/
def prodLift (f : α →. β) (g : α →. γ) : α →. β × γ := fun x =>
⟨(f x).Dom ∧ (g x).Dom, fun h => ((f x).get h.1, (g x).get h.2)⟩
