forall₃ — Mathlib

English

If f is surjective, then (forall y1,y2,y3) p(y1,y2,y3) iff (forall x1,x2,x3) p(f(x1),f(x2),f(x3)).

Русский

Если f сюръективна, то для любых y1,y2,y3 выполняется p(y1,y2,y3) тогда и только тогда, когда p(f(x1),f(x2),f(x3)) выполняется для всех x1,x2,x3.

LaTeX

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

Lean4

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

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