nil_takeUntil — Mathlib

English

For any path p from u to v, taking until the starting point u yields the empty walk.

Русский

Для любой последовательности путей p от u к v вычисление takeUntil до начала p возвращает пустой путь.

LaTeX

$$$p.takeUntil u p.start_mem_support = \text{Nil}$$$

Lean4

@[simp]
theorem nil_takeUntil (p : G.Walk u v) (hwp : w ∈ p.support) : (p.takeUntil w hwp).Nil ↔ u = w :=
  by
  refine ⟨?_, fun h => by subst h; simp⟩
  intro hnil
  cases p with
  | nil => simp only [takeUntil, eq_mpr_eq_cast] at hnil; exact hnil.eq
  | cons h q =>
    simp only [support_cons, List.mem_cons] at hwp
    obtain hl | hr := hwp
    · exact hl.symm
    · by_contra! hc
      simp [takeUntil_cons hr hc] at hnil

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