English
Let f : α ⇀ γ and g : β ⇀ δ be partial functions. Their product is the partial function f × g on α × β whose domain consists of pairs (a,b) with a ∈ Dom(f) and b ∈ Dom(g), and whose value is (f(a), g(b)).
Русский
Пусть f : α ⇀ γ и g : β ⇀ δ — частичные функции. Их произведение — частичная функция f × g на α × β, определяемая на парах (a,b) таких, что a ∈ Dom(f) и b ∈ Dom(g), и дающая значение (f(a), g(b)).
LaTeX
$$$\\text{Let } f : \\alpha \\dashrightarrow \\gamma \\text{ and } g : \\beta \\dashrightarrow \\delta. \\n\\text{Then } f \\times g : \\alpha \\times \\beta \\dashrightarrow \\gamma \\times \\delta \\text{ has }\\\\n\\quad \\operatorname{Dom}(f \\times g) = \\{(a,b) \\mid a \\in \\operatorname{Dom}(f) \\wedge b \\in \\operatorname{Dom}(g)\\},\\\\n\\quad (f \\times g)(a,b) = (f(a), g(b)) \\text{ for } (a,b) \\in \\operatorname{Dom}(f \\times g).$$$
Lean4
/-- Product of partial functions. -/
def prodMap (f : α →. γ) (g : β →. δ) : α × β →. γ × δ := fun x =>
⟨(f x.1).Dom ∧ (g x.2).Dom, fun h => ((f x.1).get h.1, (g x.2).get h.2)⟩
