edges_subset_edgeSet — Mathlib

English

Every edge in a walk is an edge of the graph, proved by induction on the walk.

Русский

Каждое ребро обхода принадлежит ребрам графа; доказательство по индукции по обходу.

LaTeX

$$$\forall p:\\ G.Walk u v,\\ e:\\ Sym2 V,\\ e \in p.\\edges \Rightarrow e \in G.edgeSet$$$

Lean4

/-- Every edge in a walk's edge list is an edge of the graph.
It is written in this form (rather than using `⊆`) to avoid unsightly coercions. -/
theorem edges_subset_edgeSet {u v : V} : ∀ (p : G.Walk u v) ⦃e : Sym2 V⦄, e ∈ p.edges → e ∈ G.edgeSet
  | cons h' p', e, h => by
    cases h
    · exact h'
    next h' => exact edges_subset_edgeSet p' h'

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