notMem_support_takeUntil_support_takeUntil_subset

English

Assume x ≠ w, w ∈ p.support, and x ∈ (p.takeUntil w hw).support. Then w is not in the support of (p.takeUntil x (p.support_takeUntil_subset hw hx)).

Русский

Пусть x ≠ w, w ∈ support(p) и x ∈ support(p.takeUntil w hw). Тогда w не принадлежит support(p.takeUntil x (p.support_takeUntil_subset hw hx)).

LaTeX

$$$ w \notin (p.takeUntil x (p.support_takeUntil_subset hw hx)).support $$$

Lean4

theorem notMem_support_takeUntil_support_takeUntil_subset {p : G.Walk u v} {w x : V} (h : x ≠ w) (hw : w ∈ p.support)
    (hx : x ∈ (p.takeUntil w hw).support) : w ∉ (p.takeUntil x (p.support_takeUntil_subset hw hx)).support :=
  by
  rw [← takeUntil_takeUntil p hw hx]
  intro hw'
  have h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length :=
    by exact length_takeUntil_lt _ h.symm
  have h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length := by exact length_takeUntil_lt _ h
  simp only [takeUntil_takeUntil] at h1 h2
  cutsat

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