edge_fiber — Mathlib

English

For any edge e of G, the set of darts whose edge is e consists exactly of the two darts that represent that edge (the dart and its symmetrization).

Русский

Для любого ребра e графа G множество дуг, соответствующих этому ребру, состоит ровно из двух дуг: самого дуга и ее симметричной дуги.

LaTeX

$$$\#{d : G.Dart \mid d.edge = e} = 2$$$

Lean4

theorem edge_fiber [DecidableEq V] (d : G.Dart) : ({d' : G.Dart | d'.edge = d.edge} : Finset _) = { d, d.symm } :=
  Finset.ext fun d' => by simpa using dart_edge_eq_iff d' d

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