ne_of_mem_support_of_append — Mathlib

English

If p.append q is a path and y ≠ v, with x ∈ p.support and y ∈ q.support, then x ≠ y.

Русский

Если p.append q — путь и y ≠ v, причём x ∈ p.support и y ∈ q.support, тогда x ≠ y.

LaTeX

$$$ (p.append q).IsPath \Rightarrow ∀ x \in p.support, ∀ y \in q.support, y \neq v \Rightarrow x \neq y $$$

Lean4

theorem ne_of_mem_support_of_append {p : G.Walk u v} {q : G.Walk v w} (hpq : (p.append q).IsPath) {x y : V}
    (hyv : y ≠ v) (hx : x ∈ p.support) (hy : y ∈ q.support) : x ≠ y :=
  by
  rintro rfl
  have hq : ¬q.Nil := by
    intro hq
    simp [nil_iff_support_eq.mp hq, hyv] at hy
  have hx' : x ∈ q.tail.support := by
    rw [support_tail_of_not_nil q hq]
    rw [mem_support_iff] at hy
    exact hy.resolve_left hyv
  exact IsPath.disjoint_support_of_append hpq hq hx hx'

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