This module provides slice notation for TreeSet slices and implements an iterator
for those slices.
@[simp]
theorem
Std.TreeSet.Raw.toList_rii
{α : Type u}
(cmp : α → α → Ordering := by exact compare)
{t : Raw α cmp}
:
theorem
Std.TreeSet.Raw.toList_ric
{α : Type u}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α cmp}
(wf : t.WF)
{bound : α}
:
Slice.toList (Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun (e : α) => (cmp e bound).isLE) t.toList
theorem
Std.TreeSet.Raw.toList_rio
{α : Type u}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α cmp}
(wf : t.WF)
{bound : α}
:
Slice.toList (Rio.Sliceable.mkSlice t *...bound) = List.filter (fun (e : α) => (cmp e bound).isLT) t.toList
theorem
Std.TreeSet.Raw.toList_rci
{α : Type u}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α cmp}
(wf : t.WF)
{bound : α}
:
Slice.toList (Rci.Sliceable.mkSlice t bound...*) = List.filter (fun (e : α) => (cmp e bound).isGE) t.toList
theorem
Std.TreeSet.Raw.toList_rco
{α : Type u}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α cmp}
(wf : t.WF)
{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
theorem
Std.TreeSet.Raw.toList_rcc
{α : Type u}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α cmp}
(wf : t.WF)
{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
theorem
Std.TreeSet.Raw.toList_roi
{α : Type u}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α cmp}
(wf : t.WF)
{bound : α}
:
Slice.toList (Roi.Sliceable.mkSlice t bound<...*) = List.filter (fun (e : α) => (cmp e bound).isGT) t.toList
theorem
Std.TreeSet.Raw.toList_roc
{α : Type u}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α cmp}
(wf : t.WF)
{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
theorem
Std.TreeSet.Raw.toList_roo
{α : Type u}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α cmp}
(wf : t.WF)
{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