class Std.Rxc.HasSize (α : Type u) : Type u

This typeclass provides support for the size function for ranges with closed lower bound (Rcc.size, Rco.size and Rci.size).

The returned size should be equal to the number of elements returned by toList. This condition is captured by the typeclass LawfulHasSize.

• size (lo hi : α) : Nat

  Returns the number of elements starting from lo that satisfy the given upper bound.

class Std.Rxc.LawfulHasSize (α : Type u) [LE α] [PRange.UpwardEnumerable α] [HasSize α] : Prop

This typeclass ensures that a HasSize instance returns the correct size for all ranges.

• size_eq_zero_of_not_le (lo hi : α) (h : ¬lo ≤ hi) : HasSize.size lo hi = 0

  If the smallest value in the range is beyond the upper bound, the size is zero.

• size_eq_one_of_succ?_eq_none (lo hi : α) (h : lo ≤ hi) (h' : PRange.succ? lo = none) : HasSize.size lo hi = 1

  If the smallest value in the range satisfies the upper bound and has no successor, the size is one.

• size_eq_succ_of_succ?_eq_some (lo hi lo' : α) (h : lo ≤ hi) (h' : PRange.succ? lo = some lo') : HasSize.size lo hi = HasSize.size lo' hi + 1

  If the smallest value in the range satisfies the upper bound and has a successor, the size is one larger than the size of the range starting at the successor.

theorem Std.Rxc.size_eq_zero_iff_not_le {α : Type u} [LE α] [PRange.UpwardEnumerable α] [HasSize α] [LawfulHasSize α] {lo hi : α} : HasSize.size lo hi = 0 ↔ ¬lo ≤ hi

theorem Std.Rxc.size_pos_iff_le {α : Type u} [LE α] [PRange.UpwardEnumerable α] [HasSize α] [LawfulHasSize α] {lo hi : α} : 0 < HasSize.size lo hi ↔ lo ≤ hi

class Std.Rxo.HasSize (α : Type u) : Type u

This typeclass provides support for the size function for ranges with open lower bound (Roc.size, Roo.size and Roi.size).

The returned size should be equal to the number of elements returned by toList. This condition is captured by the typeclass LawfulHasSize.

• size (lo hi : α) : Nat

  Returns the number of elements starting from lo that satisfy the given upper bound.

class Std.Rxo.LawfulHasSize (α : Type u) [LT α] [PRange.UpwardEnumerable α] [HasSize α] : Prop

This typeclass ensures that a HasSize instance returns the correct size for all ranges.

• size_eq_zero_of_not_le (lo hi : α) (h : ¬lo < hi) : HasSize.size lo hi = 0

  If the smallest value in the range is beyond the upper bound, the size is zero.

• size_eq_one_of_succ?_eq_none (lo hi : α) (h : lo < hi) (h' : PRange.succ? lo = none) : HasSize.size lo hi = 1

  If the smallest value in the range satisfies the upper bound and has no successor, the size is one.

• size_eq_succ_of_succ?_eq_some (lo hi lo' : α) (h : lo < hi) (h' : PRange.succ? lo = some lo') : HasSize.size lo hi = HasSize.size lo' hi + 1

  If the smallest value in the range satisfies the upper bound and has a successor, the size is one larger than the size of the range starting at the successor.

theorem Std.Rxo.size_eq_zero_iff_not_le {α : Type u} [LT α] [PRange.UpwardEnumerable α] [HasSize α] [LawfulHasSize α] {lo hi : α} : HasSize.size lo hi = 0 ↔ ¬lo < hi

theorem Std.Rxo.size_pos_iff_lt {α : Type u} [LT α] [PRange.UpwardEnumerable α] [HasSize α] [LawfulHasSize α] {lo hi : α} : 0 < HasSize.size lo hi ↔ lo < hi

class Std.Rxi.HasSize (α : Type u) : Type u

This typeclass provides support for the size function for ranges with closed lower bound (Ric.size, Rio.size and Rii.size).

The returned size should be equal to the number of elements returned by toList. This condition is captured by the typeclass LawfulHasSize.

• size (lo : α) : Nat

  Returns the number of elements starting from lo that satisfy the given upper bound.

class Std.Rxi.LawfulHasSize (α : Type u) [PRange.UpwardEnumerable α] [HasSize α] : Prop

This typeclass ensures that a HasSize instance returns the correct size for all ranges.

• size_eq_one_of_succ?_eq_none (lo : α) (h : PRange.succ? lo = none) : HasSize.size lo = 1

  If the smallest value in the range satisfies the upper bound and has no successor, the size is one.

• size_eq_succ_of_succ?_eq_some (lo lo' : α) (h : PRange.succ? lo = some lo') : HasSize.size lo = HasSize.size lo' + 1

  If the smallest value in the range satisfies the upper bound and has a successor, the size is one larger than the size of the range starting at the successor.

theorem Std.Rxi.size_pos {α : Type u} [PRange.UpwardEnumerable α] [HasSize α] [LawfulHasSize α] {lo : α} : HasSize.size lo > 0

@[inline]

def Std.Rcc.isEmpty {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] (r : Rcc α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLE instances.

Equations

• r.isEmpty = decide ¬r.lower ≤ r.upper

theorem Std.Rcc.mem_iff {α : Type u} [LE α] {r : Rcc α} {a : α} : a ∈ r ↔ r.lower ≤ a ∧ a ≤ r.upper

theorem Std.Rcc.lower_le_of_mem {α : Type u} {r : Rcc α} {a : α} [LE α] (h : a ∈ r) : r.lower ≤ a

theorem Std.Rcc.le_upper_of_mem {α : Type u} {r : Rcc α} {a : α} [LE α] (h : a ∈ r) : a ≤ r.upper

@[inline]

def Std.Rco.isEmpty {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] (r : Rco α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLT instances.

Equations

• r.isEmpty = decide ¬r.lower < r.upper

theorem Std.Rco.mem_iff {α : Type u} {r : Rco α} {a : α} [LE α] [LT α] : a ∈ r ↔ r.lower ≤ a ∧ a < r.upper

theorem Std.Rco.lower_le_of_mem {α : Type u} {r : Rco α} {a : α} [LE α] [LT α] (h : a ∈ r) : r.lower ≤ a

theorem Std.Rco.lt_upper_of_mem {α : Type u} {r : Rco α} {a : α} [LE α] [LT α] (h : a ∈ r) : a < r.upper

theorem Std.Rco.Internal.get_elem_helper_upper_open {α : Type u} {r : Rco α} {hi a : α} [LE α] [LT α] (h₁ : a ∈ r) (h₂ : r.upper = hi) : a < hi

@[inline]

def Std.Rci.isEmpty {α : Type u} [PRange.UpwardEnumerable α] : Rci α → Bool

Checks whether the range contains any value. This function exists for completeness and always returns false: The closed lower bound is contained in the range, so left-closed right-unbounded ranges are never empty.

Equations

• x✝.isEmpty = false

theorem Std.Rci.mem_iff {α : Type u} {r : Rci α} {a : α} [LE α] : a ∈ r ↔ r.lower ≤ a

theorem Std.Rci.lower_le_of_mem {α : Type u} {r : Rci α} {a : α} [LE α] (h : a ∈ r) : r.lower ≤ a

@[inline]

def Std.Roc.isEmpty {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] (r : Roc α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLT instances.

Equations

• r.isEmpty = decide ¬r.lower < r.upper

theorem Std.Roc.mem_iff {α : Type u} [LE α] [LT α] {r : Roc α} {a : α} : a ∈ r ↔ r.lower < a ∧ a ≤ r.upper

theorem Std.Roc.lower_le_of_mem {α : Type u} {r : Roc α} {a : α} [LE α] [LT α] (h : a ∈ r) : r.lower < a

theorem Std.Roc.le_upper_of_mem {α : Type u} {r : Roc α} {a : α} [LE α] [LT α] (h : a ∈ r) : a ≤ r.upper

@[inline]

def Std.Roo.isEmpty {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] (r : Roo α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLT instances.

Equations

• r.isEmpty = decide (∀ (a : α), Std.PRange.succ? r.lower = some a → ¬a < r.upper)

theorem Std.Roo.mem_iff {α : Type u} {r : Roo α} {a : α} [LT α] : a ∈ r ↔ r.lower < a ∧ a < r.upper

theorem Std.Roo.lower_le_of_mem {α : Type u} {r : Roo α} {a : α} [LT α] (h : a ∈ r) : r.lower < a

theorem Std.Roo.lt_upper_of_mem {α : Type u} {r : Roo α} {a : α} [LT α] (h : a ∈ r) : a < r.upper

theorem Std.Roo.Internal.get_elem_helper_upper_open {α : Type u} {r : Roo α} {hi a : α} [LE α] [LT α] (h₁ : a ∈ r) (h₂ : r.upper = hi) : a < hi

@[inline]

def Std.Roi.isEmpty {α : Type u} [PRange.UpwardEnumerable α] (r : Roi α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given a LawfulUpwardEnumerable instance.

Equations

• r.isEmpty = (Std.PRange.succ? r.lower).isNone

theorem Std.Roi.mem_iff {α : Type u} {r : Roi α} {a : α} [LT α] : a ∈ r ↔ r.lower < a

theorem Std.Roi.lower_le_of_mem {α : Type u} {r : Roi α} {a : α} [LT α] (h : a ∈ r) : r.lower < a

@[inline]

def Std.Ric.isEmpty {α : Type u} [PRange.UpwardEnumerable α] : Ric α → Bool

Checks whether the range contains any value. This function exists for completeness and always returns false: The closed upper bound is contained in the range, so left-unbounded right-closed ranges are never empty.

Equations

• x✝.isEmpty = false

theorem Std.Ric.mem_iff {α : Type u} {r : Ric α} {a : α} [LE α] : a ∈ r ↔ a ≤ r.upper

theorem Std.Ric.le_upper_of_mem {α : Type u} {r : Ric α} {a : α} [LE α] [LT α] (h : a ∈ r) : a ≤ r.upper

@[inline]

def Std.Rio.isEmpty {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.Least? α] (r : Rio α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable, LawfulUpwardEnumerableLT and LawfulUpwardEnumerableLeast? instances.

Equations

• r.isEmpty = decide (∀ (a : α), Std.PRange.least? = some a → ¬a < r.upper)

theorem Std.Rio.mem_iff {α : Type u} {r : Rio α} {a : α} [LT α] : a ∈ r ↔ a < r.upper

theorem Std.Rio.lt_upper_of_mem {α : Type u} {r : Rio α} {a : α} [LT α] (h : a ∈ r) : a < r.upper

theorem Std.Rio.Internal.get_elem_helper_upper_open {α : Type u} {r : Rio α} {hi a : α} [LE α] [LT α] (h₁ : a ∈ r) (h₂ : r.upper = hi) : a < hi

@[inline]

def Std.Rii.isEmpty {α : Type u} [PRange.Least? α] : Rii α → Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLeast? instances.

Equations

• x✝.isEmpty = Std.PRange.least?.isNone

theorem Std.Rii.mem {α : Type u} {r : Rii α} {a : α} : a ∈ r