English
For f : α → β → γ, p : α → Prop, q : β → Prop, r : γ → Prop, there is an equivalence: (∃ c, (∃ a, ∃ b, f a b = c) ∧ p c) ↔ ∃ a, ∃ b, p (f a b).
Русский
Для функции f: α → β → γ, p : α → Prop, q : β → Prop, r : γ → Prop существует эквивалентность: (∃ c, (∃ a, ∃ b, f a b = c) ∧ p c) ↔ ∃ a, ∃ b, p (f a b).
LaTeX
$$$$\\Big(\\exists c, (\\exists a, \\exists b, f(a,b)=c) ∧ p(c)\\Big) \\Longleftrightarrow \\exists a, \\exists b, p(f(a,b)).$$$$
Lean4
@[simp]
theorem exists_exists_exists_and_eq {α β γ : Type*} {f : α → β → γ} {p : γ → Prop} :
(∃ c, (∃ a, ∃ b, f a b = c) ∧ p c) ↔ ∃ a, ∃ b, p (f a b) :=
⟨fun ⟨_, ⟨a, b, hab⟩, hc⟩ ↦ ⟨a, b, hab.symm ▸ hc⟩, fun ⟨a, b, hab⟩ ↦ ⟨f a b, ⟨a, b, rfl⟩, hab⟩⟩
