swap_mem_interedges_iff — Mathlib

English

If r is symmetric, swapping coordinates in an edge preserves membership between interedges sets with swapped arguments.

Русский

Если r симметрична, то обмен координат ребра сохраняет принадлежность между множествами ребер с поменянными аргументами.

LaTeX

$$$\bigl(x.swap \in \operatorname{interedges}(r, s, t)\bigr) \;\Longleftrightarrow\; x \in \operatorname{interedges}(r, t, s)$ with symmetry of r$$

Lean4

@[simp]
theorem swap_mem_interedges_iff (hr : Symmetric r) {x : α × α} : x.swap ∈ interedges r s t ↔ x ∈ interedges r t s :=
  by
  rw [mem_interedges_iff, mem_interedges_iff, hr.iff]
  exact and_left_comm

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