Counting an ordered set whose values grow by at least two

Proved

EdmondsKarp.ShortestPath.card_le_of_gap_two

by arexychen · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theorynetwork-flow

For a finite set of natural-number indices and a natural-valued function bounded strictly by n on that set, if values increase by at least two between any two increasing indices, then twice the set cardinality is at most n+1.

Preamble

import Mathlib

Formal statement

theorem EdmondsKarp.ShortestPath.card_le_of_gap_two (S : Finset ℕ) (d : ℕ → ℕ) (n : ℕ)
    (hbound : ∀ k ∈ S, d k < n)
    (hgap : ∀ k ∈ S, ∀ l ∈ S, k < l → d k + 2 ≤ d l) :
    2 * S.card ≤ n + 1 := by sorry

Source

Auxiliary counting and iteration lemmas for Edmonds and Karp (1972), §1.2 p. 252. DOI: 10.1145/321694.321699.

View graph