length_ne_zero_iff_eq_cons — Mathlib

English

For any path p: a→b, p.length ≠ 0 if and only if there exist c, p' : Path a→c and e: c→b such that p = p'.cons e.

Русский

Для любого пути p: a→b, p.length ≠ 0 тогда и только тогда, когда существует c, p': Path a→c и e: c→b такие, что p = p'.cons e.

LaTeX

$$$\\forall p:\\; \\mathrm{Path}(a,b):\\; p.length \\neq 0 \\iff \\exists c:\\, V,\\; \\exists p': \\mathrm{Path}(a,c),\\; \\exists e:\\, c\\to b,\\; p = p'.cons(e).$$$

Lean4

/-- Every non-empty path can be decomposed as an initial path plus a final edge. -/
theorem length_ne_zero_iff_eq_cons : p.length ≠ 0 ↔ ∃ (c : V) (p' : Path a c) (e : c ⟶ b), p = p'.cons e :=
  by
  refine ⟨fun h ↦ ?_, ?_⟩
  ·
    cases p with
    | nil => simp at h
    | cons p' e => exact ⟨_, p', e, rfl⟩
  · rintro ⟨c, p', e, rfl⟩
    simp

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