elim — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem elim {p : Prop} {u v : V} (h : G.Reachable u v) (hp : G.Walk u v → p) : p :=
  Nonempty.elim h hp

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