forall₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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