edgesFinset — Mathlib

English

The edges of a trail form a finite set; they can be collected as a Finset of edges.

Русский

Ребра трасы образуют конечное множество; их можно рассмотреть как Finset ребер.

LaTeX

$$$ edgesFinset(h) = \langle p.edges, h.edges_nodup \rangle $$$

Lean4

/-- The edges of a trail as a finset, since each edge in a trail appears exactly once. -/
abbrev edgesFinset {u v : V} {p : G.Walk u v} (h : p.IsTrail) : Finset (Sym2 V) :=
  ⟨p.edges, h.edges_nodup⟩

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