dom_prodMap — Mathlib

English

For f : α ⇀ γ and g : β ⇀ δ, the domain of the product map f × g consists exactly of those x = (a,b) with a ∈ Dom(f) and b ∈ Dom(g).

Русский

Для частичных функций f : α ⇀ γ и g : β ⇀ δ множество определения произведения f × g равно всем парам x = (a,b), для которых a ∈ Dom(f) и b ∈ Dom(g).

LaTeX

$$$$(f \\prodMap g).\\mathrm{Dom} = \\{ x \\in \\alpha \\times \\beta \\mid (f x_1).\\Dom \\land (g x_2).\\Dom \\}.$$$$

Lean4

@[simp]
theorem dom_prodMap (f : α →. γ) (g : β →. δ) : (f.prodMap g).Dom = {x | (f x.1).Dom ∧ (g x.2).Dom} :=
  rfl

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