Suprema of downward-closed sets of natural numbers in ℕ∞

A graph invariant such as edge connectivity is often defined as the supremum in ℕ∞ of the natural thresholds n at which some property P n holds. When P is antitone (a property at n implies it at every smaller threshold) and holds at 0, the supremum recovers the property: (k : ℕ∞) ≤ ⨆ (n : ℕ) (_ : P n), (n : ℕ∞) exactly when P k.

theorem Antitone.natCast_le_iSup_iff {P : ℕ → Prop} (hP : Antitone P) (h0 : P 0) {k : ℕ} : ↑k ≤ ⨆ (n : ℕ), ⨆ (_ : P n), ↑n ↔ P k

For an antitone predicate on ℕ holding at 0, a natural number is at most the supremum in ℕ∞ of the natural numbers satisfying the predicate exactly when it satisfies the predicate.