mk_mem_sym2_iff — Mathlib

English

For a pair (x,y), the element Sym2.mk(x,y) belongs to s.sym2 exactly when (x,y) lies in s × s.

Русский

Для пары (x,y) элемент Sym2.mk(x,y) принадлежит s.sym2 тогда и только тогда, когда (x,y) принадлежит s × s.

LaTeX

$$$\\forall {x y} \\; Sym2.mk (x,y) \\in s.sym2 \\Leftrightarrow (x,y) \\in s \\times s$$$

Lean4

theorem mk_mem_sym2_iff {x y : α} : s(x, y) ∈ s.sym2 ↔ x ∈ s ∧ y ∈ s :=
  Iff.rfl

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