exists — Mathlib

English

There exists i ∈ Sym2 α such that f i holds iff there exist x,y ∈ α with f(Sym2.mk(x,y)).

Русский

Существует i ∈ Sym2 α такое, что f i, если и только если существуют x,y ∈ α такие, что f(Sym2.mk(x,y)).

LaTeX

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

Lean4

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

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