This module provides slice notation for TreeSet slices and implements an iterator for those slices.

instance Std.TreeSet.instSliceableRiiSlice {α : Type u} (cmp : α → α → Ordering := by exact compare) : Rii.Sliceable (TreeSet α cmp) α (DTreeMap.Internal.Unit.RiiSlice α)

@[simp]

theorem Std.TreeSet.toList_rii {α : Type u} (cmp : α → α → Ordering := by exact compare) {t : TreeSet α cmp} : Slice.toList (Rii.Sliceable.mkSlice t *...*) = t.toList

instance Std.TreeSet.instSliceableRicSlice {α : Type u} (cmp : α → α → Ordering := by exact compare) : Ric.Sliceable (TreeSet α cmp) α (DTreeMap.Internal.Unit.RicSlice α)

@[simp]

theorem Std.TreeSet.toList_ric {α : Type u} (cmp : α → α → Ordering := by exact compare) [TransCmp cmp] {t : TreeSet α cmp} {bound : α} : Slice.toList (Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun (e : α) => (cmp e bound).isLE) t.toList

instance Std.TreeSet.instSliceableRioSlice {α : Type u} (cmp : α → α → Ordering := by exact compare) : Rio.Sliceable (TreeSet α cmp) α (DTreeMap.Internal.Unit.RioSlice α)

@[simp]

theorem Std.TreeSet.toList_rio {α : Type u} (cmp : α → α → Ordering := by exact compare) [TransCmp cmp] {t : TreeSet α cmp} {bound : α} : Slice.toList (Rio.Sliceable.mkSlice t *...bound) = List.filter (fun (e : α) => (cmp e bound).isLT) t.toList

instance Std.TreeSet.instSliceableRciSlice {α : Type u} (cmp : α → α → Ordering := by exact compare) : Rci.Sliceable (TreeSet α cmp) α (DTreeMap.Internal.Unit.RciSlice α)

@[simp]

theorem Std.TreeSet.toList_rci {α : Type u} (cmp : α → α → Ordering := by exact compare) [TransCmp cmp] {t : TreeSet α cmp} {bound : α} : Slice.toList (Rci.Sliceable.mkSlice t bound...*) = List.filter (fun (e : α) => (cmp e bound).isGE) t.toList

instance Std.TreeSet.instSliceableRcoSlice {α : Type u} (cmp : α → α → Ordering := by exact compare) : Rco.Sliceable (TreeSet α cmp) α (DTreeMap.Internal.Unit.RcoSlice α)

@[simp]

theorem Std.TreeSet.toList_rco {α : Type u} (cmp : α → α → Ordering := by exact compare) [TransCmp cmp] {t : TreeSet α cmp} {lowerBound upperBound : α} : Slice.toList (Rco.Sliceable.mkSlice t lowerBound...upperBound) = List.filter (fun (e : α) => decide ((cmp e lowerBound).isGE = true ∧ (cmp e upperBound).isLT = true)) t.toList

instance Std.TreeSet.instSliceableRccSlice {α : Type u} (cmp : α → α → Ordering := by exact compare) : Rcc.Sliceable (TreeSet α cmp) α (DTreeMap.Internal.Unit.RccSlice α)

@[simp]

theorem Std.TreeSet.toList_rcc {α : Type u} (cmp : α → α → Ordering := by exact compare) [TransCmp cmp] {t : TreeSet α cmp} {lowerBound upperBound : α} : Slice.toList (Rcc.Sliceable.mkSlice t lowerBound...=upperBound) = List.filter (fun (e : α) => decide ((cmp e lowerBound).isGE = true ∧ (cmp e upperBound).isLE = true)) t.toList

instance Std.TreeSet.instSliceableRoiSlice {α : Type u} (cmp : α → α → Ordering := by exact compare) : Roi.Sliceable (TreeSet α cmp) α (DTreeMap.Internal.Unit.RoiSlice α)

@[simp]

theorem Std.TreeSet.toList_roi {α : Type u} (cmp : α → α → Ordering := by exact compare) [TransCmp cmp] {t : TreeSet α cmp} {bound : α} : Slice.toList (Roi.Sliceable.mkSlice t bound<...*) = List.filter (fun (e : α) => (cmp e bound).isGT) t.toList

instance Std.TreeSet.instSliceableRocSlice {α : Type u} (cmp : α → α → Ordering := by exact compare) : Roc.Sliceable (TreeSet α cmp) α (DTreeMap.Internal.Unit.RocSlice α)

@[simp]

theorem Std.TreeSet.toList_roc {α : Type u} (cmp : α → α → Ordering := by exact compare) [TransCmp cmp] {t : TreeSet α cmp} {lowerBound upperBound : α} : Slice.toList (Roc.Sliceable.mkSlice t lowerBound<...=upperBound) = List.filter (fun (e : α) => decide ((cmp e lowerBound).isGT = true ∧ (cmp e upperBound).isLE = true)) t.toList

instance Std.TreeSet.instSliceableRooSlice {α : Type u} (cmp : α → α → Ordering := by exact compare) : Roo.Sliceable (TreeSet α cmp) α (DTreeMap.Internal.Unit.RooSlice α)

@[simp]

theorem Std.TreeSet.toList_roo {α : Type u} (cmp : α → α → Ordering := by exact compare) [TransCmp cmp] {t : TreeSet α cmp} {lowerBound upperBound : α} : Slice.toList (Roo.Sliceable.mkSlice t lowerBound<...upperBound) = List.filter (fun (e : α) => decide ((cmp e lowerBound).isGT = true ∧ (cmp e upperBound).isLT = true)) t.toList