Documentation

Std.Data.Iterators.Lemmas.Producers.Range

source
@[simp]
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.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.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.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.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.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.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.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.Rii.toList_iter_eq_toList {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} :
r.iter.toList = r.toList