The least natural number satisfying a predicate, in ℕ∞

For a predicate P : ℕ → Prop, TauCeti.leastENatBound P is the infimum in ℕ∞ of the natural numbers satisfying P. It is ⊤ exactly when no natural number satisfies P, so an invariant defined as the least n for which some bound holds takes the value ⊤ rather than being undefined when no bound holds at all. Invariants of this shape are cohomological dimensions, where P n says that cohomology vanishes above degree n.

When P is monotone (a bound at m gives a bound at every n ≥ m), the characterization leastENatBound P ≤ n ↔ P n recovers the predicate from the invariant.

Main results

• TauCeti.leastENatBound: the infimum in ℕ∞ of the natural numbers satisfying a predicate.
• TauCeti.leastENatBound_le_iff: for a monotone predicate, leastENatBound P ≤ n ↔ P n.
• TauCeti.leastENatBound_eq_top_iff: the value is ⊤ exactly when the predicate never holds.
• TauCeti.leastENatBound_eq_zero_iff: the value is 0 exactly when the predicate holds at 0.
• TauCeti.leastENatBound_antitone: a weaker predicate has a smaller least bound.

noncomputable def TauCeti.leastENatBound (P : ℕ → Prop) : ℕ∞

The least natural number satisfying P, as an element of ℕ∞: the infimum of the natural numbers satisfying P, which is ⊤ when there are none.

Equations

• TauCeti.leastENatBound P = ⨅ (n : { n : ℕ // P n }), ↑↑n

theorem TauCeti.le_leastENatBound_iff {P : ℕ → Prop} {m : ℕ∞} : m ≤ leastENatBound P ↔ ∀ (n : ℕ), P n → m ≤ ↑n

A lower bound for the least bound is a lower bound for every natural number satisfying the predicate.

theorem TauCeti.leastENatBound_le {P : ℕ → Prop} {n : ℕ} (h : P n) : leastENatBound P ≤ ↑n

The least bound is at most any natural number satisfying the predicate.

@[simp]

theorem TauCeti.leastENatBound_eq_top_iff {P : ℕ → Prop} : leastENatBound P = ⊤ ↔ ∀ (n : ℕ), ¬P n

The least bound is ⊤ exactly when no natural number satisfies the predicate.

@[simp]

theorem TauCeti.leastENatBound_eq_zero_iff {P : ℕ → Prop} : leastENatBound P = 0 ↔ P 0

The least bound is 0 exactly when 0 satisfies the predicate. Unlike leastENatBound_le_iff, this needs no monotonicity.

theorem TauCeti.leastENatBound_eq_find {P : ℕ → Prop} [DecidablePred P] (h : ∃ (n : ℕ), P n) : leastENatBound P = ↑(Nat.find h)

The least bound is attained: when some natural number satisfies P, the least one does.

theorem TauCeti.leastENatBound_le_iff {P : ℕ → Prop} (hP : Monotone P) (n : ℕ) : leastENatBound P ≤ ↑n ↔ P n

For a monotone predicate, the least bound is at most n exactly when n satisfies the predicate.

theorem TauCeti.leastENatBound_antitone : Antitone leastENatBound

A weaker predicate has a smaller least bound.