dart_edge_fiber_card — Mathlib

English

The total number of darts is exactly twice the number of edges of G.

Русский

Общее число дуг графа G равно удвоенному числу рёбер графа.

LaTeX

$$$\lvert G.Dart \rvert = 2 \cdot \#G.edgeFinset$$$

Lean4

theorem dart_edge_fiber_card [DecidableEq V] (e : Sym2 V) (h : e ∈ G.edgeSet) : #{d : G.Dart | d.edge = e} = 2 :=
  by
  obtain ⟨v, w⟩ := e
  let d : G.Dart := ⟨(v, w), h⟩
  convert congr_arg card d.edge_fiber
  rw [card_insert_of_notMem, card_singleton]
  rw [mem_singleton]
  exact d.symm_ne.symm

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