support_bypass_subset — Mathlib

English

For any walk p, the support of its bypass is contained in the support of p.

Русский

Для любой обходной дорожки p опора обхода содержится в опоре самой дорожки.

LaTeX

$$$ \forall {V} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} (p : G.Walk u v), p.bypass.support \subseteq p.support$$$

Lean4

theorem support_bypass_subset {u v : V} (p : G.Walk u v) : p.bypass.support ⊆ p.support := by
  induction p with
  | nil => simp!
  | cons _ _ ih =>
    simp! only
    split_ifs
    · apply List.Subset.trans (support_dropUntil_subset _ _)
      apply List.subset_cons_of_subset
      assumption
    · rw [support_cons]
      apply List.cons_subset_cons
      assumption

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