class Std.PRange.UpwardEnumerable (α : Type u) : Type u

This typeclass provides the function succ? : α → Option α that computes the successor of elements of α, or none if no successor exists. It also provides the function succMany?, which computes n-th successors.

succ? is expected to be acyclic: No element is its own transitive successor. If α is ordered, then every element larger than a : α should be a transitive successor of a. These properties and the compatibility of succ? with succMany? are encoded in the typeclasses LawfulUpwardEnumerable, LawfulUpwardEnumerableLE and LawfulUpwardEnumerableLT.

• succ? : α → Option α

  Maps elements of α to their successor, or none if no successor exists.

• succMany? (n : Nat) (a : α) : Option α

  Maps elements of α to their n-th successor, or none if no successor exists. This should semantically behave like repeatedly applying succ?, but it might be more efficient.

  LawfulUpwardEnumerable ensures the compatibility with succ?.

  If no other implementation is provided in UpwardEnumerable instance, succMany? repeatedly applies succ?.

theorem Std.PRange.UpwardEnumerable.ext {α : Type u} {x y : UpwardEnumerable α} (succ? : succ? = succ?) (succMany? : succMany? = succMany?) : x = y

theorem Std.PRange.UpwardEnumerable.ext_iff {α : Type u} {x y : UpwardEnumerable α} : x = y ↔ succ? = succ? ∧ succMany? = succMany?

def Std.PRange.UpwardEnumerable.LE {α : Type u} [UpwardEnumerable α] (a b : α) : Prop

According to UpwardEnumerable.LE, a is less than or equal to b if b is a or a transitive successor of a.

theorem Std.PRange.UpwardEnumerable.le_iff_exists {α : Type u} {x✝ : UpwardEnumerable α} {a b : α} : UpwardEnumerable.LE a b ↔ ∃ (n : Nat), succMany? n a = some b

def Std.PRange.UpwardEnumerable.LT {α : Type u} [UpwardEnumerable α] (a b : α) : Prop

According to UpwardEnumerable.LT, a is less than b if b is a proper transitive successor of a. 'Proper' means that b is the n-th successor of a, where n > 0.

Given LawfulUpwardEnumerable α, no element of α is less than itself.

theorem Std.PRange.UpwardEnumerable.lt_iff_exists {α : Type u} [UpwardEnumerable α] {a b : α} : UpwardEnumerable.LT a b ↔ ∃ (n : Nat), succMany? (n + 1) a = some b

theorem Std.PRange.UpwardEnumerable.le_of_lt {α : Type u} [UpwardEnumerable α] {a b : α} (h : UpwardEnumerable.LT a b) : UpwardEnumerable.LE a b

class Std.PRange.Least? (α : Type u) : Type u

The typeclass Least? α optionally provides a smallest element of α, least? : Option α.

The main use case of this typeclass is to use it in combination with UpwardEnumerable to obtain a (possibly infinite) ascending enumeration of all elements of α.

• least? : Option α

  Returns the smallest element of α, or none if α is empty.

  Only empty types are allowed to define least? := none. If α is ordered and nonempty, then the value of least? should be the smallest element according to the order on α.

class Std.PRange.LawfulUpwardEnumerable (α : Type u) [UpwardEnumerable α] : Prop

This typeclass ensures that an UpwardEnumerable α instance is well-behaved.

• ne_of_lt (a b : α) : UpwardEnumerable.LT a b → a ≠ b

  There is no cyclic chain of successors.

• succMany?_zero (a : α) : succMany? 0 a = some a

  The 0-th successor of a is a itself.

• succMany?_add_one (n : Nat) (a : α) : succMany? (n + 1) a = (succMany? n a).bind succ?

  The n + 1-th successor of a is the successor of the n-th successor, given that said successors actually exist.

theorem Std.PRange.UpwardEnumerable.succMany?_zero {α : Type u_1} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a : α} : succMany? 0 a = some a

theorem Std.PRange.UpwardEnumerable.succMany?_add_one {α : Type u_1} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {n : Nat} {a : α} : succMany? (n + 1) a = (succMany? n a).bind succ?

@[deprecated Std.PRange.UpwardEnumerable.succMany?_add_one (since := "2025-09-03")]

theorem Std.PRange.UpwardEnumerable.succMany?_succ? {α : Type u_1} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {n : Nat} {a : α} : succMany? (n + 1) a = (succMany? n a).bind succ?

@[deprecated Std.PRange.UpwardEnumerable.succMany?_add_one (since := "2025-09-03")]

theorem Std.PRange.UpwardEnumerable.succMany?_succ {α : Type u_1} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {n : Nat} {a : α} : succMany? (n + 1) a = (succMany? n a).bind succ?

theorem Std.PRange.UpwardEnumerable.succMany?_one {α : Type u_1} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a : α} : succMany? 1 a = succ? a

theorem Std.PRange.UpwardEnumerable.succMany?_add {α : Type u_1} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {m n : Nat} {a : α} : succMany? (m + n) a = (succMany? m a).bind fun (x : α) => succMany? n x

theorem Std.PRange.UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany? {α : Type u_1} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {n : Nat} {a : α} : succMany? (n + 1) a = (succ? a).bind fun (x : α) => succMany? n x

@[deprecated Std.PRange.UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany? (since := "2025-09-03")]

theorem Std.PRange.UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany? {α : Type u_1} [UpwardEnumerable α] [LawfulUpwardEnumerable α] (n : Nat) (a : α) : succMany? (n + 1) a = (succ? a).bind fun (x : α) => succMany? n x

@[deprecated Std.PRange.UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany? (since := "2025-09-03")]

theorem Std.PRange.LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany? {α : Type u_1} [UpwardEnumerable α] [LawfulUpwardEnumerable α] (n : Nat) (a : α) : succMany? (n + 1) a = (succ? a).bind fun (x : α) => succMany? n x

theorem Std.PRange.UpwardEnumerable.le_refl {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] (a : α) : UpwardEnumerable.LE a a

theorem Std.PRange.UpwardEnumerable.lt_irrefl {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a : α} : ¬UpwardEnumerable.LT a a

theorem Std.PRange.UpwardEnumerable.lt_succ? {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b : α} (h : succ? a = some b) : UpwardEnumerable.LT a b

theorem Std.PRange.UpwardEnumerable.ne_of_lt {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b : α} (h : UpwardEnumerable.LT a b) : a ≠ b

theorem Std.PRange.UpwardEnumerable.le_trans {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b c : α} (hab : UpwardEnumerable.LE a b) (hbc : UpwardEnumerable.LE b c) : UpwardEnumerable.LE a c

theorem Std.PRange.UpwardEnumerable.le_of_succ?_eq {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b : α} (hab : succ? a = some b) : UpwardEnumerable.LE a b

theorem Std.PRange.UpwardEnumerable.lt_of_lt_of_le {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b c : α} (hab : UpwardEnumerable.LT a b) (hbc : UpwardEnumerable.LE b c) : UpwardEnumerable.LT a c

theorem Std.PRange.UpwardEnumerable.lt_of_le_of_lt {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b c : α} (hab : UpwardEnumerable.LE a b) (hbc : UpwardEnumerable.LT b c) : UpwardEnumerable.LT a c

theorem Std.PRange.UpwardEnumerable.lt_trans {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b c : α} (hab : UpwardEnumerable.LT a b) (hbc : UpwardEnumerable.LT b c) : UpwardEnumerable.LT a c

theorem Std.PRange.UpwardEnumerable.lt_of_le_of_ne {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b : α} (hle : UpwardEnumerable.LE a b) (hne : a ≠ b) : UpwardEnumerable.LT a b

theorem Std.PRange.UpwardEnumerable.not_gt_of_le {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b : α} : UpwardEnumerable.LE a b → ¬UpwardEnumerable.LT b a

theorem Std.PRange.UpwardEnumerable.not_ge_of_lt {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b : α} : UpwardEnumerable.LT a b → ¬UpwardEnumerable.LE b a

theorem Std.PRange.UpwardEnumerable.not_gt_of_lt {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b : α} (h : UpwardEnumerable.LT a b) : ¬UpwardEnumerable.LT b a

instance Std.PRange.instAsymmLTOfLawfulUpwardEnumerable {α : Type u_1} [UpwardEnumerable α] [LawfulUpwardEnumerable α] : Asymm UpwardEnumerable.LT

class Std.PRange.InfinitelyUpwardEnumerable (α : Type u) [UpwardEnumerable α] : Prop

This propositional typeclass ensures that UpwardEnumerable.succ? will never return none. In other words, it ensures that there will always be a successor.

• isSome_succ? (a : α) : (succ? a).isSome = true

class Std.PRange.LinearlyUpwardEnumerable (α : Type u) [UpwardEnumerable α] : Prop

This propositional typeclass ensures that UpwardEnumerable.succ? is injective.

• eq_of_succ?_eq (a b : α) : succ? a = succ? b → a = b

  The implementation of UpwardEnumerable.succ? for α is injective.

theorem Std.PRange.UpwardEnumerable.isSome_succ? {α : Type u} [UpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} : (succ? a).isSome = true

If a type is infinitely upwardly enumerable, then every element has a successor.

theorem Std.PRange.UpwardEnumerable.succ?_inj {α : Type u} [UpwardEnumerable α] [LinearlyUpwardEnumerable α] {a b : α} : succ? a = succ? b ↔ a = b

@[deprecated Std.PRange.UpwardEnumerable.succ?_inj (since := "2025-09-03")]

theorem Std.PRange.UpwardEnumerable.eq_of_succ?_eq {α : Type u} [UpwardEnumerable α] [LinearlyUpwardEnumerable α] {a b : α} (h : succ? a = succ? b) : a = b

@[reducible, inline]

abbrev Std.PRange.UpwardEnumerable.succ {α : Type u} [UpwardEnumerable α] [InfinitelyUpwardEnumerable α] (a : α) : α

Maps elements of α to their immediate successor.

theorem Std.PRange.UpwardEnumerable.succ_eq_get {α : Type u} [UpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} : succ a = (succ? a).get ⋯

theorem Std.PRange.UpwardEnumerable.succ?_eq_some {α : Type u} [UpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} : succ? a = some (succ a)

theorem Std.PRange.UpwardEnumerable.succ_inj {α : Type u} [UpwardEnumerable α] [InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] {a b : α} : succ a = succ b ↔ a = b

@[deprecated Std.PRange.UpwardEnumerable.succ_inj (since := "2025-09-03")]

theorem Std.PRange.UpwardEnumerable.eq_of_succ_eq {α : Type u} [UpwardEnumerable α] [InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] {a b : α} (h : succ a = succ b) : a = b

theorem Std.PRange.UpwardEnumerable.succ_eq_succ_iff {α : Type u} [UpwardEnumerable α] [InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] {a b : α} : succ a = succ b ↔ a = b

theorem Std.PRange.UpwardEnumerable.isSome_succMany? {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {n : Nat} {a : α} : (succMany? n a).isSome = true

@[inline]

def Std.PRange.UpwardEnumerable.succMany {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] (n : Nat) (a : α) : α

Maps elements of α to their n-th successor. This should semantically behave like repeatedly applying succ, but it might be more efficient.

This function uses an UpwardEnumerable α instance. LawfulUpwardEnumerable α ensures the compatibility with succ and succ?.

If no other implementation is provided in UpwardEnumerable instance, succMany? repeatedly applies succ?.

theorem Std.PRange.UpwardEnumerable.succMany_eq_get {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {n : Nat} {a : α} : succMany n a = (succMany? n a).get ⋯

theorem Std.PRange.UpwardEnumerable.succMany?_eq_some {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {n : Nat} {a : α} : succMany? n a = some (succMany n a)

theorem Std.PRange.UpwardEnumerable.succMany?_eq_some_iff_succMany {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {n : Nat} {a b : α} : succMany? n a = some b ↔ succMany n a = b

theorem Std.PRange.UpwardEnumerable.succMany_zero {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} : succMany 0 a = a

theorem Std.PRange.UpwardEnumerable.succMany_one {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} : succMany 1 a = succ a

theorem Std.PRange.UpwardEnumerable.succMany_succ {n : Nat} {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} : succMany (n + 1) a = succ (succMany n a)

theorem Std.PRange.UpwardEnumerable.succMany_add_one_eq_succMany_succ {n : Nat} {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} : succMany (n + 1) a = succMany n (succ a)

theorem Std.PRange.UpwardEnumerable.succMany_succ_eq_succ_succMany {n : Nat} {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} : succMany n (succ a) = succ (succMany n a)

theorem Std.PRange.UpwardEnumerable.succMany_add {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {m n : Nat} {a : α} : succMany (m + n) a = succMany n (succMany m a)

theorem Std.PRange.UpwardEnumerable.lt_succ {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} : UpwardEnumerable.LT a (succ a)

theorem Std.PRange.UpwardEnumerable.succ_le_succ {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a b : α} (h : UpwardEnumerable.LE a b) : UpwardEnumerable.LE (succ a) (succ b)

theorem Std.PRange.UpwardEnumerable.succ_le_succ_iff {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] {a b : α} : UpwardEnumerable.LE (succ a) (succ b) ↔ UpwardEnumerable.LE a b

theorem Std.PRange.UpwardEnumerable.succ_lt_succ {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a b : α} (h : UpwardEnumerable.LT a b) : UpwardEnumerable.LT (succ a) (succ b)

theorem Std.PRange.UpwardEnumerable.succ_lt_succ_iff {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] {a b : α} : UpwardEnumerable.LT (succ a) (succ b) ↔ UpwardEnumerable.LT a b

class Std.PRange.LawfulUpwardEnumerableLE (α : Type u) [UpwardEnumerable α] [LE α] : Prop

This typeclass ensures that an UpwardEnumerable α instance is compatible with ≤. In this case, UpwardEnumerable α fully characterizes the LE α instance.

• le_iff (a b : α) : a ≤ b ↔ UpwardEnumerable.LE a b

  a is less than or equal to b if and only if b is either a or a transitive successor of a.

theorem Std.PRange.UpwardEnumerable.le_iff {α : Type u} [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] {a b : α} : a ≤ b ↔ UpwardEnumerable.LE a b

def Std.PRange.UpwardEnumerable.instLETransOfLawfulUpwardEnumerableLE {α : Type u} [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] : Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2

class Std.PRange.LawfulUpwardEnumerableLT (α : Type u) [UpwardEnumerable α] [LT α] : Prop

This typeclass ensures that an UpwardEnumerable α instance is compatible with <. In this case, UpwardEnumerable α fully characterizes the LT α instance.

• lt_iff (a b : α) : a < b ↔ UpwardEnumerable.LT a b

  a is less than b if and only if b is a proper transitive successor of a.

theorem Std.PRange.UpwardEnumerable.lt_iff {α : Type u} [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] {a b : α} : a < b ↔ UpwardEnumerable.LT a b

theorem Std.PRange.UpwardEnumerable.le_iff_lt_or_eq {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a b : α} : UpwardEnumerable.LE a b ↔ UpwardEnumerable.LT a b ∨ a = b

theorem Std.PRange.UpwardEnumerable.succ_le_iff {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a b : α} : UpwardEnumerable.LE (succ a) b ↔ UpwardEnumerable.LT a b

theorem Std.PRange.UpwardEnumerable.lt_succ_iff {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] {a b : α} : UpwardEnumerable.LT a (succ b) ↔ UpwardEnumerable.LE a b

def Std.PRange.UpwardEnumerable.instLTTransOfLawfulUpwardEnumerableLT {α : Type u} [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] : Trans (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : α) => x1 < x2

def Std.PRange.UpwardEnumerable.instLawfulOrderLTOfLawfulUpwardEnumerableLT {α : Type u} [LT α] [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLE α] : LawfulOrderLT α

class Std.PRange.LawfulUpwardEnumerableLeast? (α : Type u) [UpwardEnumerable α] [Least? α] : Prop

This typeclass ensures that an UpwardEnumerable α instance is compatible with a Least? α instance. For nonempty α, it ensures that least? has a value and that every other value is a transitive successor of it.

• least?_le (a : α) : ∃ (init : α), least? = some init ∧ UpwardEnumerable.LE init a

  For nonempty α, least? has a value and every other value is a transitive successor of it.

theorem Std.PRange.UpwardEnumerable.least?_le {α : Type u} [UpwardEnumerable α] [Least? α] [LawfulUpwardEnumerableLeast? α] {a : α} : ∃ (init : α), least? = some init ∧ UpwardEnumerable.LE init a

theorem Std.PRange.UpwardEnumerable.isSome_least? {α : Type u} [UpwardEnumerable α] [Least? α] [LawfulUpwardEnumerableLeast? α] [hn : Nonempty α] : least?.isSome = true

def Std.PRange.UpwardEnumerable.least {α : Type u_1} [UpwardEnumerable α] [Least? α] [LawfulUpwardEnumerableLeast? α] [hn : Nonempty α] : α

theorem Std.PRange.UpwardEnumerable.least_le {α : Type u_1} [UpwardEnumerable α] [Least? α] [LawfulUpwardEnumerableLeast? α] {a : α} : UpwardEnumerable.LE least a

theorem Std.PRange.UpwardEnumerable.least?_eq_some {α : Type u} [UpwardEnumerable α] [Least? α] [LawfulUpwardEnumerableLeast? α] [hn : Nonempty α] : least? = some least

theorem Std.PRange.UpwardEnumerable.isSome_least?_iff {α : Type u} [UpwardEnumerable α] [Least? α] [LawfulUpwardEnumerableLeast? α] : least?.isSome = true ↔ Nonempty α

theorem Std.PRange.UpwardEnumerable.least?_eq_none_iff {α : Type u} [UpwardEnumerable α] [Least? α] [LawfulUpwardEnumerableLeast? α] : least? = none ↔ ¬Nonempty α