forall — Mathlib

English

For any f : Sym2 α → Prop, (∀ x:Sym2 α, f x) is equivalent to ∀ x,y, f(Sym2.mk(x,y)).

Русский

Для любого f : Sym2 α → Prop, верно равенство (∀ x:Sym2 α, f x) ↔ ∀ x,y, f(Sym2.mk(x,y)).

LaTeX

$$$$ (\forall x:Sym2\alpha, f\,x) \iff (\forall x,y, f(\mathrm{Sym2.mk}\{fst := x, snd := y\})). $$$$

Lean4

protected theorem «forall» {α : Sort _} {f : Sym2 α → Prop} : (∀ x : Sym2 α, f x) ↔ ∀ x y, f s(x, y) :=
  mk_surjective.forall.trans Prod.forall

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