Successor inequalities in ℕ∞

Depth inequalities for a short exact sequence 0 → A → B → C → 0 bound one depth below by the minimum of the other two, shifted by one. This file collects the ℕ∞ arithmetic that combines such bounds into equalities.

Main results

• ENat.le_of_inf_le_of_inf_le: if c ⊓ (b + 1) ≤ a and c ⊓ (a + 1) ≤ b, then c ≤ a.
• ENat.add_succ_eq_of_le_of_le: the bounds (b + p) ⊓ (b - 1) ≤ a and a + 1 ≤ b give a + (p + 1) = b + p.

theorem ENat.le_of_inf_le_of_inf_le {a b c : ℕ∞} (ha : min c (b + 1) ≤ a) (hb : min c (a + 1) ≤ b) : c ≤ a

If c ⊓ (b + 1) ≤ a and c ⊓ (a + 1) ≤ b, then c ≤ a.

theorem ENat.add_succ_eq_of_le_of_le {a b : ℕ∞} {p : ℕ} (h₁ : min (b + ↑p) (b - 1) ≤ a) (h₂ : a + 1 ≤ b) : a + ↑(p + 1) = b + ↑p

If (b + p) ⊓ (b - 1) ≤ a and a + 1 ≤ b, then a + (p + 1) = b + p.