notNilRec_cons — Mathlib

English

NotNil is equivalent to the existence of a decomposition p = cons h q with some adjacent h.

Русский

NotNil эквивално существованию разложения p = cons h q с некоторым смежным h.

LaTeX

$$$ \neg p.Nil \iff \exists u,h,q:\ p = q.\cons h $$$

Lean4

@[simp]
theorem notNilRec_cons {motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort*}
    (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (q.cons h) Walk.not_nil_cons) (h' : G.Adj u v)
    (q' : G.Walk v w) : @Walk.notNilRec _ _ _ _ _ cons _ _ = cons h' q' := by rfl

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