getVert_le_length_takeUntil_eq_iff

English

For h ∈ p.support and hn : n ≤ (p.takeUntil u h).length, we have p.getVert n = u iff n = (p.takeUntil u h).length.

Русский

Для h ∈ поддержка(p) и hn : n ≤ длина(p.takeUntil u h), имеем p.getVert n = u тогда и только тогда, когда n = длина(p.takeUntil u h).length.

LaTeX

$$$$ p.getVert n = u \iff n = (p.takeUntil u h).length $$$$

Lean4

theorem getVert_le_length_takeUntil_eq_iff {n : ℕ} {p : G.Walk v w} (h : u ∈ p.support)
    (hn : n ≤ (p.takeUntil _ h).length) : p.getVert n = u ↔ n = (p.takeUntil _ h).length := by
  grind [getVert_length_takeUntil, getVert_lt_length_takeUntil_ne]

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