darts_bypass_subset — Mathlib

English

The bypass of a walk's darts is a subset of the original darts.

Русский

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

LaTeX

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

Lean4

theorem darts_bypass_subset {u v : V} (p : G.Walk u v) : p.bypass.darts ⊆ p.darts := by
  induction p with
  | nil => simp!
  | cons _ _ ih =>
    simp! only
    split_ifs
    · apply List.Subset.trans (darts_dropUntil_subset _ _)
      apply List.subset_cons_of_subset _ ih
    · rw [darts_cons]
      exact List.cons_subset_cons _ ih

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