elim_path — Mathlib

English

If u is reachable from v and a property holds for every walk from u to v, then that property holds.

Русский

Пусть u достижим из v; тогда, если некое свойство выполняется для каждого хода от u до v, оно выполняется.

LaTeX

$$$G.Reachable u v \to (\forall w: G.Walk u v, p) \to p$$$

Lean4

protected theorem elim_path {p : Prop} {u v : V} (h : G.Reachable u v) (hp : G.Path u v → p) : p := by
  classical exact h.elim fun q => hp q.toPath

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