swap_mem_interedges_iff — Mathlib

English

If you swap the two coordinates of a pair, membership in interedges corresponds to membership in the swapped interedges set.

Русский

Если поменять координаты пары, принадлежность к interedges s t эквивалентна принадлежности к interedges t s для swap.

LaTeX

$$x.swap ∈ G.interedges s t ↔ x ∈ G.interedges t s$$

Lean4

@[simp]
theorem swap_mem_interedges_iff {x : α × α} : x.swap ∈ G.interedges s t ↔ x ∈ G.interedges t s :=
  Rel.swap_mem_interedges_iff G.symm

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