card_interedges_comm — Mathlib

English

The number of edges between s and t equals the number of edges between t and s after a swap, i.e., symmetry of interedges counts.

Русский

Число ребер между s и t равно числу ребер между t и s после обмена, т.е. симметрия счёта ребер.

LaTeX

$$$\#(\operatorname{interedges}(r, s, t)) = \#(\operatorname{interedges}(r, t, s))$$$

Lean4

theorem card_interedges_comm (hr : Symmetric r) (s t : Finset α) : #(interedges r s t) = #(interedges r t s) :=
  Finset.card_bij (fun (x : α × α) _ ↦ x.swap) (fun _ ↦ (swap_mem_interedges_iff hr).2)
    (fun _ _ _ _ h ↦ Prod.swap_injective h) fun x h ↦ ⟨x.swap, (swap_mem_interedges_iff hr).2 h, x.swap_swap⟩

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