English
For a function f: α → β, predicates p on α and q on β, there is an equivalence between (∃ b, (∃ a, p a ∧ f a = b) ∧ q b) and (∃ a, p a ∧ q (f a)).
Русский
Для функции f: α → β и предикатов p на α и q на β существует эквивалентность между (∃ b, (∃ a, p a ∧ f a = b) ∧ q b) и (∃ a, p a ∧ q (f a)).
LaTeX
$$$$\\Big(\\exists b,\\big(\\exists a, p(a) \\land f(a)=b\\big) \\land q(b)\\Big) \\Longleftrightarrow \\exists a, p(a) \\land q(f(a)).$$$$
Lean4
@[simp]
theorem exists_exists_and_eq_and {f : α → β} {p : α → Prop} {q : β → Prop} :
(∃ b, (∃ a, p a ∧ f a = b) ∧ q b) ↔ ∃ a, p a ∧ q (f a) :=
⟨fun ⟨_, ⟨a, ha, hab⟩, hb⟩ ↦ ⟨a, ha, hab.symm ▸ hb⟩, fun ⟨a, hp, hq⟩ ↦ ⟨f a, ⟨a, hp, rfl⟩, hq⟩⟩
