length_lt — Mathlib

English

Let G be a finite-type graph with vertex set V. For any path p from u to v, the length of p is less than the number of vertices: length(p) < |V|.

Русский

Пусть граф G имеет конечное множество вершин V. Для любого пути p от u до v выполняется length(p) < |V|.

LaTeX

$$p.IsPath \Rightarrow p.length < |V|$$

Lean4

theorem length_lt [Fintype V] {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.length < Fintype.card V :=
  by
  rw [Nat.lt_iff_add_one_le, ← length_support]
  exact hp.support_nodup.length_le_card

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