snd_takeUntil — Mathlib

English

If w ≠ u and w ∈ p.support, then the second element of p.takeUntil w h equals the second element of p: (p.takeUntil w h).snd = p.snd.

Русский

Если w ≠ u и w ∈ поддержка p, тогда второй элемент p.takeUntil w h равен второму элементу p: (p.takeUntil w h).snd = p.snd.

LaTeX

$$$ (p.takeUntil w h).snd = p.snd $$$

Lean4

theorem snd_takeUntil (hsu : w ≠ u) (p : G.Walk u v) (h : w ∈ p.support) : (p.takeUntil w h).snd = p.snd :=
  by
  apply p.getVert_takeUntil h
  by_contra! hc
  simp only [Nat.lt_one_iff, ← nil_iff_length_eq, nil_takeUntil] at hc
  exact hsu hc.symm

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