mk_mem_interedges_comm — Mathlib

English

If symmetry holds, then swapping a and b in an edge corresponds exactly to swapping the two finite sets on the sides.

Русский

При симметрии обмен a и b в ребре точно соответствует обмену множеств по сторонам.

LaTeX

$$$(a,b) \in \operatorname{interedges}(r, s, t) \iff (b,a) \in \operatorname{interedges}(r, t, s)$$$

Lean4

theorem mk_mem_interedges_comm (hr : Symmetric r) : (a, b) ∈ interedges r s t ↔ (b, a) ∈ interedges r t s :=
  @swap_mem_interedges_iff _ _ _ _ _ hr (b, a)

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