exists₃ — Mathlib

English

If f is surjective, then there exists y1,y2,y3 such that p holds iff there exist x1,x2,x3 with p(f(x1),f(x2),f(x3)).

Русский

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

LaTeX

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

Lean4

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

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