Documentation

Std.Data.Iterators.Lemmas.Producers.Range

source
@[simp]
theorem Std.Rcc.toList_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rcc α} :
r.iter.toList = r.toList
source
@[deprecated Std.Rcc.toList_iter (since := "2025-11-13")]
theorem Std.Rcc.toList_iter_eq_toList {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rcc α} :
r.iter.toList = r.toList
source
@[simp]
theorem Std.Rcc.toArray_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rcc α} :
r.iter.toArray = r.toArray
source
@[deprecated Std.Rcc.toArray_iter (since := "2025-11-13")]
theorem Std.Rcc.toArray_iter_eq_toArray {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rcc α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Rcc.count_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Rcc α} :
r.iter.count = r.size
source
@[deprecated Std.Rcc.count_iter (since := "2025-11-13")]
theorem Std.Rcc.count_iter_eq_size {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Rcc α} :
r.iter.count = r.size
source
@[simp]
theorem Std.Rco.toList_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rco α} :
r.iter.toList = r.toList
source
@[deprecated Std.Rco.toList_iter (since := "2025-11-13")]
theorem Std.Rco.toList_iter_eq_toList {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rco α} :
r.iter.toList = r.toList
source
@[simp]
theorem Std.Rco.toArray_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rco α} :
r.iter.toArray = r.toArray
source
@[deprecated Std.Rco.toArray_iter (since := "2025-11-13")]
theorem Std.Rco.toArray_iter_eq_toArray {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rco α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Rco.count_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Rco α} :
r.iter.count = r.size
source
@[deprecated Std.Rco.count_iter (since := "2025-11-13")]
theorem Std.Rco.count_iter_eq_size {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Rco α} :
r.iter.count = r.size
source
@[simp]
theorem Std.Rci.toList_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} :
r.iter.toList = r.toList
source
@[deprecated Std.Rci.toList_iter (since := "2025-11-13")]
theorem Std.Rci.toList_iter_eq_toList {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} :
r.iter.toList = r.toList
source
@[simp]
theorem Std.Rci.toArray_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Rci.toArray_iter_eq_toArray {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Rci.count_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rci α} :
r.iter.count = r.size
source
@[deprecated Std.Rci.count_iter (since := "2025-11-13")]
theorem Std.Rci.count_iter_eq_size {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rci α} :
r.iter.count = r.size
source
@[simp]
theorem Std.Roc.toList_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roc α} :
r.iter.toList = r.toList
source
@[deprecated Std.Roc.toList_iter (since := "2025-11-13")]
theorem Std.Roc.toList_iter_eq_toList {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roc α} :
r.iter.toList = r.toList
source
@[simp]
theorem Std.Roc.toArray_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roc α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Roc.toArray_iter_eq_toArray {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roc α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Roc.count_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Roc α} :
r.iter.count = r.size
source
@[deprecated Std.Roc.count_iter (since := "2025-11-13")]
theorem Std.Roc.count_iter_eq_size {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Roc α} :
r.iter.count = r.size
source
@[simp]
theorem Std.Roo.toList_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roo α} :
r.iter.toList = r.toList
source
@[deprecated Std.Roo.toList_iter (since := "2025-11-13")]
theorem Std.Roo.toList_iter_eq_toList {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roo α} :
r.iter.toList = r.toList
source
@[simp]
theorem Std.Roo.toArray_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roo α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Roo.toArray_iter_eq_toArray {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roo α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Roo.count_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Roo α} :
r.iter.count = r.size
source
@[deprecated Std.Roo.count_iter (since := "2025-11-13")]
theorem Std.Roo.count_iter_eq_size {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Roo α} :
r.iter.count = r.size
source
@[simp]
theorem Std.Roi.toList_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roi α} :
r.iter.toList = r.toList
source
@[deprecated Std.Roi.toList_iter (since := "2025-11-13")]
theorem Std.Roi.toList_iter_eq_toList {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roi α} :
r.iter.toList = r.toList
source
@[simp]
theorem Std.Roi.toArray_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roi α} :
r.iter.toArray = r.toArray
source
@[deprecated Std.Roi.toArray_iter (since := "2025-11-13")]
theorem Std.Roi.toArray_iter_eq_toArray {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roi α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Roi.count_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Roi α} :
r.iter.count = r.size
source
@[deprecated Std.Roi.count_iter (since := "2025-11-13")]
theorem Std.Roi.count_iter_eq_size {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Roi α} :
r.iter.count = r.size
source
@[simp]
theorem Std.Ric.toList_iter {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Ric α} :
r.iter.toList = r.toList
source
@[deprecated Std.Ric.toList_iter (since := "2025-11-13")]
theorem Std.Ric.toList_iter_eq_toList {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Ric α} :
r.iter.toList = r.toList
source
@[simp]
theorem Std.Ric.toArray_iter {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Ric α} :
r.iter.toArray = r.toArray
source
@[deprecated Std.Ric.toArray_iter (since := "2025-11-13")]
theorem Std.Ric.toArray_iter_eq_toArray {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Ric α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Ric.count_iter {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Ric α} :
r.iter.count = r.size
source
@[deprecated Std.Ric.count_iter (since := "2025-11-13")]
theorem Std.Ric.count_iter_eq_size {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Ric α} :
r.iter.count = r.size
source
@[simp]
theorem Std.Rio.toList_iter {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rio α} :
r.iter.toList = r.toList
source
@[deprecated Std.Rio.toList_iter (since := "2025-11-13")]
theorem Std.Rio.toList_iter_eq_toList {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rio α} :
r.iter.toList = r.toList
source
@[simp]
theorem Std.Rio.toArray_iter {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rio α} :
r.iter.toArray = r.toArray
source
@[deprecated Std.Rio.toArray_iter (since := "2025-11-13")]
theorem Std.Rio.toArray_iter_eq_toArray {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rio α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Rio.count_iter {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Rio α} :
r.iter.count = r.size
source
@[deprecated Std.Rio.count_iter (since := "2025-11-13")]
theorem Std.Rio.count_iter_eq_size {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Rio α} :
r.iter.count = r.size
source
@[simp]
theorem Std.Rii.toList_iter {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} :
r.iter.toList = r.toList
source
@[deprecated Std.Rii.toList_iter (since := "2025-11-13")]
theorem Std.Rii.toList_iter_eq_toList {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} :
r.iter.toList = r.toList
source
@[simp]
theorem Std.Rii.toArray_iter {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} :
r.iter.toArray = r.toArray
source
@[deprecated Std.Rii.toArray_iter (since := "2025-11-13")]
theorem Std.Rii.toArray_iter_eq_toArray {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} :
r.iter.toArray = r.toArray
source
@[simp]
theorem Std.Rii.count_iter {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rii α} :
r.iter.count = r.size
source
@[deprecated Std.Rii.count_iter (since := "2025-11-13")]
theorem Std.Rii.count_iter_eq_size {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rii α} :
r.iter.count = r.size