isLink_iff_sym2_eq — Mathlib

English

If h: G.IsLink e x y, then for any x',y', G.IsLink e x' y' is equivalent to Sym2(x,y) = Sym2(x',y').

Русский

Если h: IsLink e x y, то для любых x',y' IsLink e x' y' равносильно тому, что Sym2(x,y) = Sym2(x',y').

LaTeX

$$$G.IsLink\\,e\\,x\\,y \\rightarrow \\forall x',y', G.IsLink\\,e\\,x'\\,y' \\leftrightarrow \\operatorname{Sym2}(x,y)=\\operatorname{Sym2}(x',y').$$$

Lean4

theorem isLink_iff_sym2_eq (h : G.IsLink e x y) {x' y' : α} : G.IsLink e x' y' ↔ s(x, y) = s(x', y') := by
  rw [h.isLink_iff, Sym2.eq_iff]

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