English
Membership in f.prodLift g at x for a pair y = (y1, y2) is equivalent to y1 ∈ f x and y2 ∈ g x; equivalently, y ∈ f.prodLift g x iff y.fst ∈ f x and y.snd ∈ g x.
Русский
Членство пары y = (y1, y2) в f.prodLift g x эквивалентно y1 ∈ f x и y2 ∈ g x; то есть y ∈ f.prodLift g x ⇔ y.fst ∈ f x и y.snd ∈ g x.
LaTeX
$$$$ y \in f.prodLift g x \iff y.1 \in f x \land y.2 \in g x. $$$$
Lean4
theorem mem_prodLift {f : α →. β} {g : α →. γ} {x : α} {y : β × γ} : y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x :=
by
trans ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2
· simp only [prodLift, Part.mem_mk_iff, And.exists, Prod.ext_iff]
· simp only [exists_and_left, exists_and_right, Membership.mem, Part.Mem]
