dart_fst_mem_support_of_mem_darts

English

If a dart d belongs to the list p.darts, then its first coordinate d.fst is in the support of p.

Русский

Если дуга d принадлежит списку p.darts, то первая компонента d.fst принадлежит поддержке p.

LaTeX

$$$ \forall p:\ G.Walk\,u\,v, \forall d:\ G.Dart, d \in p.darts \Rightarrow d.fst \in p.support $$$

Lean4

theorem dart_fst_mem_support_of_mem_darts {u v : V} : ∀ (p : G.Walk u v) {d : G.Dart}, d ∈ p.darts → d.fst ∈ p.support
  | cons h p', d, hd => by
    simp only [support_cons, darts_cons, List.mem_cons] at hd ⊢
    rcases hd with (rfl | hd)
    · exact Or.inl rfl
    · exact Or.inr (dart_fst_mem_support_of_mem_darts _ hd)

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