coe_edges_toFinset — Mathlib

English

For any walk p, the set of edges represented by p.edges as a Finset corresponds exactly to p.edgeSet.

Русский

Для любого хода p множество рёбер, представленных p.edges как множество Finset, точно равно p.edgeSet.

LaTeX

$$$ (p.edges.toFinset) = p.edgeSet $$$

Lean4

theorem coe_edges_toFinset [DecidableEq V] {u v : V} (p : G.Walk u v) : (p.edges.toFinset : Set (Sym2 V)) = p.edgeSet :=
  by simp [edgeSet]

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