exists₂ — Mathlib

English

If f is surjective, then (exists y1,y2) p(y1,y2) iff (exists x1,x2) p(f(x1),f(x2)).

Русский

Если f сюръективна, то существует y1,y2 такие, что p(y1,y2) тогда и только тогда, существует x1,x2 такие, что p(f(x1),f(x2)).

LaTeX

$$$\\operatorname{Surjective}(f) \\rightarrow (\\exists y_1 y_2, p(y_1,y_2) \\iff \\exists x_1 x_2, p(f(x_1),f(x_2)))$$$

Lean4

protected theorem exists₂ (hf : Surjective f) {p : β → β → Prop} : (∃ y₁ y₂, p y₁ y₂) ↔ ∃ x₁ x₂, p (f x₁) (f x₂) :=
  hf.exists.trans <| exists_congr fun _ ↦ hf.exists

Похожие утверждения