English
A pair y = (y1,y2) is in f.prodMap g at x = (x1,x2) if and only if y1 ∈ f x1 and y2 ∈ g x2.
Русский
Пара y = (y1,y2) принадлежит f.prodMap g в точке x = (x1,x2) тогда и только тогда, когда y1 ∈ f x1 и y2 ∈ g x2.
LaTeX
$$$$ y \\in f.prodMap g x \\iff y_1 \\in f x_1 \\wedge y_2 \\in g x_2. $$$$
Lean4
theorem mem_prodMap {f : α →. γ} {g : β →. δ} {x : α × β} {y : γ × δ} : y ∈ f.prodMap g x ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2 :=
by
trans ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2
· simp only [prodMap, Part.mem_mk_iff, And.exists, Prod.ext_iff]
· simp only [exists_and_left, exists_and_right, Membership.mem, Part.Mem]
