length_le_card_edgeFinset — Mathlib

English

If e is in p.edges, then e appears exactly once in p.edges.

Русский

Если ребро e встречается в p.edges, то оно встречается ровно один раз.

LaTeX

$$$ e \in p.edges \Rightarrow p.edges.count(e) = 1 $$$

Lean4

theorem length_le_card_edgeFinset [Fintype G.edgeSet] {u v : V} {w : G.Walk u v} (h : w.IsTrail) :
    w.length ≤ G.edgeFinset.card := by
  classical
  let edges := w.edges.toFinset
  have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup
  rw [← this]
  have : edges ⊆ G.edgeFinset := by
    intro e h
    refine mem_edgeFinset.mpr ?_
    apply w.edges_subset_edgeSet
    simpa [edges] using h
  exact Finset.card_le_card this

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