English
Let f: α → β, p : α → Prop, q : β → Prop, r : γ → Prop. Then there is an equivalence between (∃ c, (∃ a, p a ∧ ∃ b, q b ∧ f a b = c) ∧ r c) and (∃ a, p a ∧ ∃ b, q b ∧ r (f a b)).
Русский
Пусть f: α → β, p: α → Prop, q: β → Prop, r: γ → Prop. Тогда существует эквивалентность между (∃ c, (∃ a, p a ∧ ∃ b, q b ∧ f a b = c) ∧ r c) и (∃ a, p a ∧ ∃ b, q b ∧ r (f a b)).
LaTeX
$$$$\\Big(\\exists c,\\big(\\exists a, p(a) ∧ \\exists b, q(b) ∧ f(a,b)=c\\big) ∧ r(c)\\Big) \\\\Longleftrightarrow \\exists a, p(a) ∧ \\exists b, q(b) ∧ r(f(a,b)).$$$$
Lean4
@[simp]
theorem exists_exists_and_exists_and_eq_and {α β γ : Type*} {f : α → β → γ} {p : α → Prop} {q : β → Prop}
{r : γ → Prop} : (∃ c, (∃ a, p a ∧ ∃ b, q b ∧ f a b = c) ∧ r c) ↔ ∃ a, p a ∧ ∃ b, q b ∧ r (f a b) :=
⟨fun ⟨_, ⟨a, ha, b, hb, hab⟩, hc⟩ ↦ ⟨a, ha, b, hb, hab.symm ▸ hc⟩, fun ⟨a, ha, b, hb, hab⟩ ↦
⟨f a b, ⟨a, ha, b, hb, rfl⟩, hab⟩⟩
