Lemmas

📁 Source: Batteries/Data/RBMap/Lemmas.lean

Statistics

Metric	Count
Definitions IsCut, IsStrictCut, AllL, AllR, listL, listR, withList, delRoot, instDecidableOrderedOfTransCmp, setRoot, instDecidableMemOfTransCmp	11
Theorems contains_iff_find?, contains_iff_findEntry?, default_eq, empty_eq, empty_toList, find?_congr, find?_insert, find?_insert_of_eq, find?_insert_of_ne, find?_some, find?_some_mem_toList, findEntry?_congr, findEntry?_insert, findEntry?_insert_of_eq, findEntry?_insert_of_ne, findEntry?_some, findEntry?_some_eq_eq, findEntry?_some_mem_toList, foldlM_eq_foldlM_toList, foldl_eq_foldl_toList, foldr_eq_foldr_toList, forIn_eq_forIn_toList, forM_eq_forM_toList, instIsStrictCut, instIsStrictCutByKeyOfTransCmp, mem_toList, mem_toList_insert, mem_toList_insert_of_mem, mem_toList_insert_self, mem_toList_unique, mkRBSet_eq, single_toList, size_eq, toList_sorted, toStream_eq, toStream_toList, val_toList, lowerBound?, lowerBound?_lb, upperBound?, upperBound?_ub, All_def, Any_def, Any_reverse, gt_trans, le_gt_trans, le_lt_trans, lt_trans, exact, toIsCut, Mem_reverse, find?_some, le_max?, lowerBound?_exists, lowerBound?_greatest, lowerBound?_greatest_lb, lowerBound?_lt, lt_upperBound?, memP_iff_find?, memP_iff_lowerBound?, memP_iff_upperBound?, min?_le, toList_sorted, unique, upperBound?_exists, upperBound?_least, upperBound?_least_ub, insert, erase, insert, fill_toList, ins_eq_fill, ins_toList, insertNew_eq_insert, insertNew_toList, insert_toList, ordered_iff, rootOrdered_iff, zoom_del, zoom_ins, zoom_insert, zoom_zoomed₁, foldl_eq_foldl_toList, foldr_cons, foldr_eq_foldr_toList, forIn_eq_forIn_toList, next?_toList, toList_cons, toList_nil, balLeft_toList, balRight_toList, balance1_toList, balance2_toList, exists_find?_insert_self, exists_insert_toList_zoom_nil, exists_insert_toList_zoom_node, find?_insert_self, find?_reverse, find?_some_eq_eq, find?_some_mem, find?_some_memP, foldlM_eq_foldlM_toList, foldl_eq_foldl_toList, foldl_reverse, foldr_cons, foldr_eq_foldr_toList, foldr_reverse, forIn_eq_forIn_toList, forIn_visit_eq_bindList, forM_eq_forM_toList, insert_toList_zoom, insert_toList_zoom_nil, insert_toList_zoom_node, instIsCutFlipOrderingSwap, instIsStrictCut, instIsStrictCutFlipOrderingSwap, isOrdered_iff, isOrdered_iff', lowerBound?_eq_find?, lowerBound?_le, lowerBound?_le', lowerBound?_mem, lowerBound?_mem_lb, lowerBound?_of_some, lowerBound?_reverse, max?_eq_toList_getLast?, max?_mem, max?_reverse, memP_def, memP_reverse, mem_congr, mem_def, mem_insert, mem_insert_of_mem, mem_insert_self, mem_nil, mem_node, mem_reverse, mem_toList, min?_eq_toList_head?, min?_mem, min?_reverse, ordered_iff, reverse_size, setBlack_toList, setRed_toList, size_eq, toList_nil, toList_node, toList_reverse, toStream_toList, toStream_toList', upperBound?_eq_find?, upperBound?_ge, upperBound?_ge', upperBound?_mem, upperBound?_mem_ub, upperBound?_of_some, upperBound?_reverse, zoom_toList, contains_iff, default_eq, empty_eq, empty_toList, find?_congr, find?_insert, find?_insert_of_eq, find?_insert_of_ne, find?_some, find?_some_eq_eq, find?_some_mem, find?_some_mem_toList, findP?_insert, findP?_insert_of_eq, findP?_insert_of_ne, findP?_some, findP?_some_eq_eq, findP?_some_memP, findP?_some_mem_toList, foldlM_eq_foldlM_toList, foldl_eq_foldl_toList, foldr_eq_foldr_toList, forIn_eq_forIn_toList, forM_eq_forM_toList, isEmpty_iff_toList_eq_nil, lowerBound?_eq_find?, lowerBound?_exists, lowerBound?_le, lowerBound?_lt, lowerBound?_mem, lowerBound?_mem_toList, lowerBoundP?_eq_findP?, lowerBoundP?_exists, lowerBoundP?_greatest, lowerBoundP?_le, lowerBoundP?_lt, lowerBoundP?_mem, lowerBoundP?_mem_toList, lt_upperBound?, lt_upperBoundP?, memP_iff_findP?, memP_iff_lowerBoundP?, memP_iff_upperBoundP?, mem_congr, mem_iff_find?, mem_iff_lowerBound?, mem_iff_mem_toList, mem_iff_upperBound?, mem_insert, mem_insert_of_eq, mem_insert_of_mem, mem_insert_of_mem_toList, mem_insert_self, mem_of_mem_toList, mem_toList, mem_toList_insert, mem_toList_insert_of_mem, mem_toList_insert_self, mem_toList_unique, mkRBSet_eq, single_toList, size_eq, toList_sorted, toStream_eq, toStream_toList, upperBound?_eq_find?, upperBound?_exists, upperBound?_ge, upperBound?_mem, upperBound?_mem_toList, upperBoundP?_eq_findP?, upperBoundP?_exists, upperBoundP?_ge, upperBoundP?_least, upperBoundP?_mem, upperBoundP?_mem_toList, val_toList	237
Total	248

Batteries.RBMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contains_iff_find? 📖	bridging (iff)	—	contains find?	contains	—
contains_iff_findEntry? 📖	bridging (iff)	—	contains findEntry?	contains	—
default_eq 📖	mathematical	—	Batteries.RBMap Batteries.instInhabitedRBMap Batteries.instEmptyCollectionRBMap	—	—
empty_eq 📖	mathematical	—	empty Batteries.RBMap Batteries.instEmptyCollectionRBMap	—	—
empty_toList 📖	mathematical	—	toList Batteries.RBMap Batteries.instEmptyCollectionRBMap	—	—
find?_congr 📖	mathematical	—	find?	—	findEntry?_congr
find?_insert 📖	mathematical	—	find? insert	—	find?_insert_of_ne find?_insert_of_eq
find?_insert_of_eq 📖	mathematical	—	find? insert	—	find?.eq_1 findEntry?_insert_of_eq
find?_insert_of_ne 📖	mathematical	—	find? insert	—	findEntry?_insert_of_ne
find?_some 📖	mathematical	—	find? toList	—	—
find?_some_mem_toList 📖	mathematical	find?	toList	—	findEntry?_some_mem_toList findEntry?_some_eq_eq
findEntry?_congr 📖	mathematical	—	findEntry?	—	—
findEntry?_insert 📖	mathematical	—	findEntry? insert	—	Batteries.RBSet.findP?_insert Std.instTransCmpByKey instIsStrictCutByKeyOfTransCmp
findEntry?_insert_of_eq 📖	mathematical	—	findEntry? insert	—	Batteries.RBSet.findP?_insert_of_eq Std.instTransCmpByKey instIsStrictCutByKeyOfTransCmp
findEntry?_insert_of_ne 📖	mathematical	—	findEntry? insert	—	Batteries.RBSet.findP?_insert_of_ne Std.instTransCmpByKey instIsStrictCutByKeyOfTransCmp
findEntry?_some 📖	mathematical	—	findEntry? toList	—	Batteries.RBSet.findP?_some Std.instTransCmpByKey instIsStrictCutByKeyOfTransCmp
findEntry?_some_eq_eq 📖	—	findEntry?	—	—	Batteries.RBSet.findP?_some_eq_eq
findEntry?_some_mem_toList 📖	mathematical	findEntry?	toList	—	Batteries.RBSet.findP?_some_mem_toList
foldlM_eq_foldlM_toList 📖	mathematical	—	foldlM toList	—	Batteries.RBNode.foldlM_eq_foldlM_toList
foldl_eq_foldl_toList 📖	mathematical	—	foldl toList	—	Batteries.RBNode.foldl_eq_foldl_toList
foldr_eq_foldr_toList 📖	mathematical	—	foldr toList	—	Batteries.RBNode.foldr_eq_foldr_toList
forIn_eq_forIn_toList 📖	mathematical	—	Batteries.RBMap instForInProdOfMonad toList	—	Batteries.RBNode.forIn_eq_forIn_toList
forM_eq_forM_toList 📖	mathematical	—	forM toList	—	Batteries.RBNode.forM_eq_forM_toList
instIsStrictCut 📖	mathematical	—	Batteries.RBNode.IsStrictCut	—	Std.TransCmp.lt_of_lt_of_le Std.TransCmp.le_trans
instIsStrictCutByKeyOfTransCmp 📖	mathematical	—	Batteries.RBNode.IsStrictCut Ordering.byKey	—	Std.TransCmp.lt_of_lt_of_le Std.TransCmp.le_trans
mem_toList 📖	mathematical	—	toList Batteries.RBNode Batteries.RBNode.instMembership Batteries.RBNode.WF Ordering.byKey	—	Batteries.RBNode.mem_toList
mem_toList_insert 📖	mathematical	—	toList insert	—	Batteries.RBSet.mem_toList_insert Std.instTransCmpByKey
mem_toList_insert_of_mem 📖	mathematical	toList	insert	—	Batteries.RBSet.mem_toList_insert_of_mem
mem_toList_insert_self 📖	mathematical	—	toList insert	—	Batteries.RBSet.mem_toList_insert_self
mem_toList_unique 📖	—	toList	—	—	Batteries.RBSet.mem_toList_unique Std.instTransCmpByKey
mkRBSet_eq 📖	mathematical	—	Batteries.mkRBMap Batteries.RBMap Batteries.instEmptyCollectionRBMap	—	—
single_toList 📖	mathematical	—	toList single	—	—
size_eq 📖	mathematical	—	size toList	—	Batteries.RBNode.size_eq
toList_sorted 📖	mathematical	—	Batteries.RBNode.cmpLT toList	—	Batteries.RBSet.toList_sorted
toStream_eq 📖	mathematical	—	Batteries.RBMap Batteries.RBNode.Stream instToStreamStreamProd Batteries.RBNode.toStream Batteries.RBNode Batteries.RBNode.WF Ordering.byKey Batteries.RBNode.Stream.nil	—	—
toStream_toList 📖	mathematical	—	Batteries.RBNode.Stream.toList Batteries.RBMap Batteries.RBNode.Stream instToStreamStreamProd toList	—	Batteries.RBSet.toStream_toList
val_toList 📖	mathematical	—	Batteries.RBNode.toList Batteries.RBNode Batteries.RBNode.WF Ordering.byKey toList	—	—

Batteries.RBNode

Definitions

Name	Category	Theorems
IsCut 📖	CompData	2 math math: IsStrictCut.toIsCut, instIsCutFlipOrderingSwap
IsStrictCut 📖	CompData	4 math math: instIsStrictCut, Batteries.RBMap.instIsStrictCutByKeyOfTransCmp, instIsStrictCutFlipOrderingSwap, Batteries.RBMap.instIsStrictCut
delRoot 📖	CompOp	1 math math: Path.zoom_del
instDecidableOrderedOfTransCmp 📖	CompOp	—
setRoot 📖	CompOp	3 math math: insert_toList_zoom, Path.zoom_ins, Path.insert_toList

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
All_def 📖	mathematical	—	All	—	—
Any_def 📖	mathematical	—	Any Batteries.RBNode instMembership	—	—
Any_reverse 📖	mathematical	—	Any reverse	—	—
Mem_reverse 📖	mathematical	—	Mem reverse	—	—
balLeft_toList 📖	mathematical	—	toList balLeft	—	toList_node balance2_toList setRed_toList
balRight_toList 📖	mathematical	—	toList balRight	—	toList_node balance1_toList setRed_toList
balance1_toList 📖	mathematical	—	toList balance1	—	toList_node
balance2_toList 📖	mathematical	—	toList balance2	—	toList_node
exists_find?_insert_self 📖	mathematical	Balanced Ordered	find? insert	—	Ordered.memP_iff_find? Ordered.insert memP_def mem_insert_self
exists_insert_toList_zoom_nil 📖	mathematical	Balanced zoom Path.root Batteries.RBNode Path nil	toList insert	—	zoom_toList insert_toList_zoom_nil
exists_insert_toList_zoom_node 📖	mathematical	Balanced zoom Path.root Batteries.RBNode Path node	toList insert	—	zoom_toList toList_node insert_toList_zoom_node
find?_insert_self 📖	mathematical	Balanced Ordered	find? insert	—	Ordered.find?_some Ordered.insert mem_insert_self
find?_reverse 📖	mathematical	—	find? reverse	—	—
find?_some_eq_eq 📖	—	find?	—	—	—
find?_some_mem 📖	mathematical	find?	Batteries.RBNode instMembership	—	—
find?_some_memP 📖	mathematical	find?	MemP	—	memP_def find?_some_mem find?_some_eq_eq
foldlM_eq_foldlM_toList 📖	mathematical	—	foldlM toList	—	toList_node
foldl_eq_foldl_toList 📖	mathematical	—	foldl toList	—	toList_node
foldl_reverse 📖	mathematical	—	foldl reverse foldr	—	foldl_eq_foldl_toList toList_reverse foldr_eq_foldr_toList
foldr_cons 📖	mathematical	—	foldr toList	—	foldr.eq_2
foldr_eq_foldr_toList 📖	mathematical	—	foldr toList	—	toList_node
foldr_reverse 📖	mathematical	—	foldr reverse foldl	—	foldl_reverse reverse_reverse
forIn_eq_forIn_toList 📖	mathematical	—	Batteries.RBNode instForInOfMonad toList	—	List.forIn_eq_bindList forIn_visit_eq_bindList
forIn_visit_eq_bindList 📖	mathematical	—	forIn.visit ForInStep.bindList toList	—	ForInStep.bind_yield_bindList toList_node ForInStep.bindList_append
forM_eq_forM_toList 📖	mathematical	—	forM toList	—	toList_node
insert_toList_zoom 📖	mathematical	Balanced zoom Path.root Batteries.RBNode Path	toList insert Path.withList setRoot	—	setBlack_toList Path.zoom_insert Path.insert_toList
insert_toList_zoom_nil 📖	mathematical	Balanced zoom Path.root Batteries.RBNode Path nil	toList insert Path.withList	—	insert_toList_zoom
insert_toList_zoom_node 📖	mathematical	Balanced zoom Path.root Batteries.RBNode Path node	toList insert Path.withList	—	insert_toList_zoom
instIsCutFlipOrderingSwap 📖	mathematical	—	IsCut	—	Std.instTransCmpFlipOrdering_batteries IsCut.le_gt_trans IsCut.le_lt_trans
instIsStrictCut 📖	mathematical	—	IsStrictCut	—	Std.TransCmp.lt_of_lt_of_le Std.TransCmp.le_trans
instIsStrictCutFlipOrderingSwap 📖	mathematical	—	IsStrictCut	—	instIsCutFlipOrderingSwap IsStrictCut.toIsCut Std.instTransCmpFlipOrdering_batteries IsStrictCut.exact
isOrdered_iff 📖	bridging (iff)	—	isOrdered Ordered	isOrdered	—
isOrdered_iff' 📖	bridging (iff)	—	isOrdered All cmpLT Ordered	isOrdered	cmpLT.trans_l cmpLT.trans_r cmpLT.trans
lowerBound?_eq_find? 📖	mathematical	find?	lowerBound?	—	reverse_reverse lowerBound?_reverse upperBound?_eq_find? find?_reverse
lowerBound?_le 📖	—	lowerBound?	—	—	lowerBound?_le'
lowerBound?_le' 📖	—	lowerBound?	—	—	reverse_reverse lowerBound?_reverse upperBound?_ge'
lowerBound?_mem 📖	mathematical	lowerBound?	Batteries.RBNode instMembership	—	lowerBound?_mem_lb
lowerBound?_mem_lb 📖	mathematical	lowerBound?	Batteries.RBNode instMembership	—	All.lowerBound?_lb All_def
lowerBound?_of_some 📖	mathematical	—	lowerBound?	—	reverse_reverse lowerBound?_reverse upperBound?_of_some
lowerBound?_reverse 📖	mathematical	—	lowerBound? reverse upperBound?	—	reverse_reverse upperBound?_reverse
max?_eq_toList_getLast? 📖	mathematical	—	max? toList	—	min?_reverse min?_eq_toList_head? toList_reverse
max?_mem 📖	mathematical	max?	Batteries.RBNode instMembership	—	min?_mem min?_reverse
max?_reverse 📖	mathematical	—	max? reverse min?	—	min?_reverse reverse_reverse
memP_def 📖	mathematical	—	MemP Batteries.RBNode instMembership	—	Any_def
memP_reverse 📖	mathematical	—	MemP reverse	—	—
mem_congr 📖	mathematical	—	Mem	—	Mem.eq_1
mem_def 📖	mathematical	—	Mem Batteries.RBNode instMembership	—	Any_def
mem_insert 📖	mathematical	Balanced Ordered	Batteries.RBNode instMembership insert	—	exists_insert_toList_zoom_nil find?_eq_zoom exists_insert_toList_zoom_node Ordered.toList_sorted mem_insert_of_mem Ordered.find?_some instIsStrictCut mem_insert_self
mem_insert_of_mem 📖	mathematical	Balanced Batteries.RBNode instMembership	insert	—	exists_insert_toList_zoom_nil exists_insert_toList_zoom_node Path.zoom_zoomed₁
mem_insert_self 📖	mathematical	Balanced	Batteries.RBNode instMembership insert	—	mem_toList exists_insert_toList_zoom_nil exists_insert_toList_zoom_node
mem_nil 📖	mathematical	—	Batteries.RBNode instMembership nil	—	—
mem_node 📖	mathematical	—	Batteries.RBNode instMembership node	—	—
mem_reverse 📖	mathematical	—	Batteries.RBNode instMembership reverse	—	mem_toList toList_reverse
mem_toList 📖	mathematical	—	toList Batteries.RBNode instMembership	—	toList_node
min?_eq_toList_head? 📖	mathematical	—	min? toList	—	toList_node
min?_mem 📖	mathematical	min?	Batteries.RBNode instMembership	—	mem_toList min?_eq_toList_head?
min?_reverse 📖	mathematical	—	min? reverse max?	—	max?.eq_def min?.eq_def
ordered_iff 📖	mathematical	—	Ordered cmpLT toList	—	toList_node cmpLT.trans
reverse_size 📖	mathematical	—	size reverse	—	size_eq toList_reverse
setBlack_toList 📖	mathematical	—	toList setBlack	—	toList_node
setRed_toList 📖	mathematical	—	toList setRed	—	toList_node
size_eq 📖	mathematical	—	size toList	—	toList_node
toList_nil 📖	mathematical	—	toList nil	—	—
toList_node 📖	mathematical	—	toList node	—	toList.eq_1 foldr.eq_2 foldr_cons
toList_reverse 📖	mathematical	—	toList reverse	—	toList_node
toStream_toList 📖	mathematical	—	Stream.toList toStream Stream.nil toList	—	toStream_toList'
toStream_toList' 📖	mathematical	—	Stream.toList toStream toList	—	Stream.toList_cons toList_node
upperBound?_eq_find? 📖	mathematical	find?	upperBound?	—	—
upperBound?_ge 📖	—	upperBound?	—	—	upperBound?_ge'
upperBound?_ge' 📖	—	upperBound?	—	—	—
upperBound?_mem 📖	mathematical	upperBound?	Batteries.RBNode instMembership	—	upperBound?_mem_ub
upperBound?_mem_ub 📖	mathematical	upperBound?	Batteries.RBNode instMembership	—	All.upperBound?_ub All_def
upperBound?_of_some 📖	mathematical	—	upperBound?	—	—
upperBound?_reverse 📖	mathematical	—	upperBound? reverse lowerBound?	—	—
zoom_toList 📖	mathematical	zoom Path.root Batteries.RBNode Path	Path.withList toList	—	Path.fill_toList Path.zoom_fill

Batteries.RBNode.All

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lowerBound? 📖	—	Batteries.RBNode.All Batteries.RBNode.lowerBound?	—	—	lowerBound?_lb
lowerBound?_lb 📖	—	Batteries.RBNode.All Batteries.RBNode.lowerBound?	—	—	Batteries.RBNode.reverse_reverse Batteries.RBNode.lowerBound?_reverse upperBound?_ub reverse
upperBound? 📖	—	Batteries.RBNode.All Batteries.RBNode.upperBound?	—	—	upperBound?_ub
upperBound?_ub 📖	—	Batteries.RBNode.All Batteries.RBNode.upperBound?	—	—	—

Batteries.RBNode.IsCut

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gt_trans 📖	—	—	—	—	le_gt_trans
le_gt_trans 📖	—	—	—	—	—
le_lt_trans 📖	—	—	—	—	—
lt_trans 📖	—	—	—	—	le_lt_trans

Batteries.RBNode.IsStrictCut

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact 📖	—	—	—	—	—
toIsCut 📖	mathematical	—	Batteries.RBNode.IsCut	—	—

Batteries.RBNode.Ordered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
find?_some 📖	mathematical	Batteries.RBNode.Ordered	Batteries.RBNode.find? Batteries.RBNode Batteries.RBNode.instMembership	—	Batteries.RBNode.find?_some_mem Batteries.RBNode.find?_some_eq_eq memP_iff_find? Batteries.RBNode.IsStrictCut.toIsCut Batteries.RBNode.memP_def unique Batteries.RBNode.IsStrictCut.exact
le_max? 📖	—	Batteries.RBNode.Ordered Batteries.RBNode.max? Batteries.RBNode Batteries.RBNode.instMembership	—	—	min?_le Std.instTransCmpFlipOrdering_batteries reverse Batteries.RBNode.min?_reverse
lowerBound?_exists 📖	mathematical	Batteries.RBNode.Ordered	Batteries.RBNode.lowerBound? Batteries.RBNode Batteries.RBNode.instMembership	—	Batteries.RBNode.reverse_reverse Batteries.RBNode.lowerBound?_reverse Batteries.RBNode.upperBound?_reverse upperBound?_exists Std.instTransCmpFlipOrdering_batteries Batteries.RBNode.instIsCutFlipOrderingSwap reverse
lowerBound?_greatest 📖	—	Batteries.RBNode.Ordered Batteries.RBNode.lowerBound? Batteries.RBNode Batteries.RBNode.instMembership	—	—	lowerBound?_greatest_lb
lowerBound?_greatest_lb 📖	—	Batteries.RBNode.Ordered Batteries.RBNode.All Batteries.RBNode.cmpLT Batteries.RBNode.lowerBound? Batteries.RBNode Batteries.RBNode.instMembership	—	—	upperBound?_least_ub Std.instTransCmpFlipOrdering_batteries Batteries.RBNode.instIsCutFlipOrderingSwap reverse Batteries.RBNode.All.reverse Batteries.RBNode.All.imp Batteries.RBNode.cmpLT.flip Batteries.RBNode.lowerBound?_reverse Batteries.RBNode.reverse_reverse
lowerBound?_lt 📖	—	Batteries.RBNode.Ordered Batteries.RBNode.lowerBound? Batteries.RBNode Batteries.RBNode.instMembership	—	—	Batteries.RBNode.lowerBound?_le Batteries.RBNode.IsStrictCut.exact lowerBound?_greatest Batteries.RBNode.IsStrictCut.toIsCut Batteries.RBNode.IsCut.le_lt_trans
lt_upperBound? 📖	—	Batteries.RBNode.Ordered Batteries.RBNode.upperBound? Batteries.RBNode Batteries.RBNode.instMembership	—	—	lowerBound?_lt Std.instTransCmpFlipOrdering_batteries Batteries.RBNode.instIsStrictCutFlipOrderingSwap reverse Batteries.RBNode.upperBound?_reverse Batteries.RBNode.reverse_reverse
memP_iff_find? 📖	mathematical	Batteries.RBNode.Ordered	Batteries.RBNode.MemP Batteries.RBNode.find?	—	Batteries.RBNode.Any_def Batteries.RBNode.IsCut.lt_trans Batteries.RBNode.All_def Batteries.RBNode.IsCut.gt_trans Batteries.RBNode.find?_some_memP
memP_iff_lowerBound? 📖	mathematical	Batteries.RBNode.Ordered	Batteries.RBNode.MemP Batteries.RBNode.lowerBound?	—	Batteries.RBNode.memP_def lowerBound?_exists Batteries.RBNode.lowerBound?_le lowerBound?_greatest Batteries.RBNode.IsCut.congr Batteries.RBNode.IsCut.gt_trans Batteries.RBNode.lowerBound?_mem
memP_iff_upperBound? 📖	mathematical	Batteries.RBNode.Ordered	Batteries.RBNode.MemP Batteries.RBNode.upperBound?	—	Batteries.RBNode.memP_def upperBound?_exists Batteries.RBNode.IsCut.lt_trans Batteries.RBNode.IsCut.congr upperBound?_least Batteries.RBNode.upperBound?_ge Batteries.RBNode.upperBound?_mem
min?_le 📖	—	Batteries.RBNode.Ordered Batteries.RBNode.min? Batteries.RBNode Batteries.RBNode.instMembership	—	—	toList_sorted Batteries.RBNode.min?_eq_toList_head? Batteries.RBNode.mem_toList
toList_sorted 📖	mathematical	Batteries.RBNode.Ordered	Batteries.RBNode.cmpLT Batteries.RBNode.toList	—	Batteries.RBNode.ordered_iff
unique 📖	—	Batteries.RBNode.Ordered Batteries.RBNode Batteries.RBNode.instMembership	—	—	Batteries.RBNode.All_def Batteries.RBNode.cmpLT.trans
upperBound?_exists 📖	mathematical	Batteries.RBNode.Ordered	Batteries.RBNode.upperBound? Batteries.RBNode Batteries.RBNode.instMembership	—	Batteries.RBNode.upperBound?_mem Batteries.RBNode.upperBound?_ge Batteries.RBNode.upperBound?_of_some Batteries.RBNode.IsCut.gt_trans Batteries.RBNode.All_def
upperBound?_least 📖	—	Batteries.RBNode.Ordered Batteries.RBNode.upperBound? Batteries.RBNode Batteries.RBNode.instMembership	—	—	upperBound?_least_ub
upperBound?_least_ub 📖	—	Batteries.RBNode.Ordered Batteries.RBNode.All Batteries.RBNode.cmpLT Batteries.RBNode.upperBound? Batteries.RBNode Batteries.RBNode.instMembership	—	—	Batteries.RBNode.upperBound?_mem_ub Batteries.RBNode.All_def Batteries.RBNode.IsCut.gt_trans

Batteries.RBNode.Path

Definitions

Name	Category	Theorems
AllL 📖	MathDef	—
AllR 📖	MathDef	—
listL 📖	CompOp	1 math math: ordered_iff
listR 📖	CompOp	1 math math: ordered_iff
withList 📖	CompOp	8 math math: fill_toList, insertNew_toList, Batteries.RBNode.zoom_toList, Batteries.RBNode.insert_toList_zoom, ins_toList, Batteries.RBNode.insert_toList_zoom_nil, insert_toList, Batteries.RBNode.insert_toList_zoom_node

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fill_toList 📖	mathematical	—	Batteries.RBNode.toList fill withList	—	Batteries.RBNode.toList_node
ins_eq_fill 📖	mathematical	Balanced Batteries.RBNode.Balanced	ins Batteries.RBNode.setBlack fill	—	ins.eq_def ins.eq_4 fill.eq_2 Batteries.RBNode.balance1_eq ins.eq_5 fill.eq_3 Batteries.RBNode.balance2_eq
ins_toList 📖	mathematical	—	Batteries.RBNode.toList ins withList	—	Batteries.RBNode.setBlack_toList Batteries.RBNode.toList_node Batteries.RBNode.balance1_toList Batteries.RBNode.balance2_toList
insertNew_eq_insert 📖	mathematical	Batteries.RBNode.zoom root Batteries.RBNode Batteries.RBNode.Path Batteries.RBNode.nil	insertNew Batteries.RBNode.setBlack Batteries.RBNode.insert	—	zoom_ins Batteries.RBNode.insert_setBlack
insertNew_toList 📖	mathematical	—	Batteries.RBNode.toList insertNew withList	—	ins_toList Batteries.RBNode.toList_node
insert_toList 📖	mathematical	—	Batteries.RBNode.toList insert withList Batteries.RBNode.setRoot	—	insertNew_toList Batteries.RBNode.toList_node fill_toList
ordered_iff 📖	mathematical	—	Ordered Batteries.RBNode.cmpLT listL listR	—	Ordered.eq_2 rootOrdered_iff Ordered.eq_3
rootOrdered_iff 📖	mathematical	Ordered	RootOrdered Batteries.RBNode.cmpLT	—	Batteries.RBNode.cmpLT.trans
zoom_del 📖	mathematical	Batteries.RBNode.zoom Batteries.RBNode Batteries.RBNode.Path	del Batteries.RBNode.del Batteries.RBColor Batteries.RBColor.red Batteries.RBNode.delRoot	—	—
zoom_ins 📖	mathematical	Batteries.RBNode.zoom Batteries.RBNode Batteries.RBNode.Path	ins Batteries.RBNode.ins Batteries.RBNode.setRoot	—	—
zoom_insert 📖	mathematical	Batteries.RBNode.Balanced Batteries.RBNode.zoom root Batteries.RBNode Batteries.RBNode.Path	Batteries.RBNode.setBlack insert Batteries.RBNode.insert	—	Batteries.RBNode.Balanced.zoom insertNew_eq_insert Batteries.RBNode.setBlack_idem ins_eq_fill Batteries.RBNode.insert_setBlack zoom_ins
zoom_zoomed₁ 📖	mathematical	Batteries.RBNode.zoom Batteries.RBNode Batteries.RBNode.Path	Batteries.RBNode.OnRoot	—	Batteries.RBNode.zoom.eq_def

Batteries.RBNode.Path.Balanced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
insert 📖	mathematical	Batteries.RBNode.Path.Balanced Batteries.RBNode.Balanced	Batteries.RBNode.Path.insert	—	insertNew fill

Batteries.RBNode.Path.Ordered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
erase 📖	mathematical	Batteries.RBNode.Path.Ordered Batteries.RBNode.Ordered Batteries.RBNode.All Batteries.RBNode.Path.RootOrdered	Batteries.RBNode.Path.erase	—	fill del Batteries.RBNode.Ordered.append Batteries.RBNode.All.append
insert 📖	mathematical	Batteries.RBNode.Path.Ordered Batteries.RBNode.Ordered Batteries.RBNode.All Batteries.RBNode.Path.RootOrdered Batteries.RBNode.OnRoot Batteries.RBNode.cmpEq	Batteries.RBNode.Path.insert	—	insertNew fill Batteries.RBNode.All.imp Batteries.RBNode.cmpEq.lt_congr_right Batteries.RBNode.cmpEq.lt_congr_left

Batteries.RBNode.Stream

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
foldl_eq_foldl_toList 📖	mathematical	—	foldl toList	—	Batteries.RBNode.foldl_eq_foldl_toList toList_cons
foldr_cons 📖	mathematical	—	foldr toList	—	Batteries.RBNode.foldr_cons
foldr_eq_foldr_toList 📖	mathematical	—	foldr toList	—	Batteries.RBNode.foldr_eq_foldr_toList toList_cons
forIn_eq_forIn_toList 📖	mathematical	—	Batteries.RBNode Batteries.RBNode.instForInOfMonad Batteries.RBNode.toList	—	List.forIn_eq_bindList Batteries.RBNode.forIn_visit_eq_bindList
next?_toList 📖	mathematical	—	Batteries.RBNode.Stream toList next? List.next?	—	Batteries.RBNode.toStream_toList' toList_cons
toList_cons 📖	mathematical	—	toList cons Batteries.RBNode.toList	—	toList.eq_1 foldr.eq_2 Batteries.RBNode.foldr_cons
toList_nil 📖	mathematical	—	toList nil	—	—

Batteries.RBSet

Definitions

Name	Category	Theorems
instDecidableMemOfTransCmp 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contains_iff 📖	bridging (iff)	—	contains Batteries.RBSet instMembership	contains	mem_iff_find?
default_eq 📖	mathematical	—	Batteries.RBSet instInhabited instEmptyCollection	—	—
empty_eq 📖	mathematical	—	empty Batteries.RBSet instEmptyCollection	—	—
empty_toList 📖	mathematical	—	toList Batteries.RBSet instEmptyCollection	—	—
find?_congr 📖	mathematical	—	find?	—	—
find?_insert 📖	mathematical	—	find? insert	—	findP?_insert Batteries.RBNode.instIsStrictCut
find?_insert_of_eq 📖	mathematical	—	find? insert	—	findP?_insert_of_eq Batteries.RBNode.instIsStrictCut
find?_insert_of_ne 📖	mathematical	—	find? insert	—	findP?_insert_of_ne Batteries.RBNode.instIsStrictCut
find?_some 📖	mathematical	—	find? toList	—	findP?_some Batteries.RBNode.instIsStrictCut
find?_some_eq_eq 📖	—	find?	—	—	findP?_some_eq_eq
find?_some_mem 📖	mathematical	find?	Batteries.RBSet instMembership	—	findP?_some_memP
find?_some_mem_toList 📖	mathematical	find?	toList	—	findP?_some_mem_toList
findP?_insert 📖	mathematical	—	findP? insert	—	findP?_insert_of_ne findP?_insert_of_eq
findP?_insert_of_eq 📖	mathematical	—	findP? insert	—	findP?_some mem_toList_insert_self
findP?_insert_of_ne 📖	mathematical	—	findP? insert	—	findP?_some mem_toList_insert Batteries.RBNode.IsCut.congr Batteries.RBNode.IsStrictCut.toIsCut find?_some_eq_eq
findP?_some 📖	mathematical	—	findP? toList	—	Batteries.RBNode.Ordered.find?_some Batteries.RBNode.WF.out
findP?_some_eq_eq 📖	—	findP?	—	—	Batteries.RBNode.find?_some_eq_eq
findP?_some_memP 📖	mathematical	findP?	MemP	—	Batteries.RBNode.find?_some_memP
findP?_some_mem_toList 📖	mathematical	findP?	toList	—	mem_toList Batteries.RBNode.find?_some_mem
foldlM_eq_foldlM_toList 📖	mathematical	—	foldlM toList	—	Batteries.RBNode.foldlM_eq_foldlM_toList
foldl_eq_foldl_toList 📖	mathematical	—	foldl toList	—	Batteries.RBNode.foldl_eq_foldl_toList
foldr_eq_foldr_toList 📖	mathematical	—	foldr toList	—	Batteries.RBNode.foldr_eq_foldr_toList
forIn_eq_forIn_toList 📖	mathematical	—	Batteries.RBSet instForInOfMonad toList	—	Batteries.RBNode.forIn_eq_forIn_toList
forM_eq_forM_toList 📖	mathematical	—	forM toList	—	Batteries.RBNode.forM_eq_forM_toList
isEmpty_iff_toList_eq_nil 📖	bridging (iff)	—	isEmpty toList	isEmpty	Batteries.RBNode.toList_node
lowerBound?_eq_find? 📖	mathematical	find?	lowerBound?	—	lowerBoundP?_eq_findP?
lowerBound?_exists 📖	mathematical	—	lowerBound? Batteries.RBSet instMembership	—	lowerBoundP?_exists Batteries.RBNode.IsStrictCut.toIsCut Batteries.RBNode.instIsStrictCut
lowerBound?_le 📖	—	lowerBound?	—	—	lowerBoundP?_le
lowerBound?_lt 📖	—	lowerBound? Batteries.RBSet instMembership	—	—	lowerBoundP?_lt Batteries.RBNode.instIsStrictCut
lowerBound?_mem 📖	mathematical	lowerBound?	Batteries.RBSet instMembership	—	lowerBoundP?_mem
lowerBound?_mem_toList 📖	mathematical	lowerBound?	toList	—	lowerBoundP?_mem_toList
lowerBoundP?_eq_findP? 📖	mathematical	findP?	lowerBoundP?	—	Batteries.RBNode.lowerBound?_eq_find?
lowerBoundP?_exists 📖	mathematical	—	lowerBoundP? Batteries.RBSet instMembership	—	Batteries.RBNode.Ordered.lowerBound?_exists Batteries.RBNode.WF.out Batteries.RBNode.IsCut.congr
lowerBoundP?_greatest 📖	—	lowerBoundP? Batteries.RBSet instMembership	—	—	mem_iff_mem_toList Batteries.RBNode.Ordered.lowerBound?_greatest Batteries.RBNode.WF.out mem_toList Batteries.RBNode.IsCut.congr
lowerBoundP?_le 📖	—	lowerBoundP?	—	—	Batteries.RBNode.lowerBound?_le
lowerBoundP?_lt 📖	—	lowerBoundP? Batteries.RBSet instMembership	—	—	mem_iff_mem_toList Batteries.RBNode.Ordered.lowerBound?_lt Batteries.RBNode.WF.out mem_toList Batteries.RBNode.IsCut.congr Batteries.RBNode.IsStrictCut.toIsCut
lowerBoundP?_mem 📖	mathematical	lowerBoundP?	Batteries.RBSet instMembership	—	mem_of_mem_toList lowerBoundP?_mem_toList
lowerBoundP?_mem_toList 📖	mathematical	lowerBoundP?	toList	—	mem_toList Batteries.RBNode.lowerBound?_mem
lt_upperBound? 📖	—	upperBound? Batteries.RBSet instMembership	—	—	lt_upperBoundP? Batteries.RBNode.instIsStrictCut
lt_upperBoundP? 📖	—	upperBoundP? Batteries.RBSet instMembership	—	—	mem_iff_mem_toList Batteries.RBNode.Ordered.lt_upperBound? Batteries.RBNode.WF.out mem_toList Batteries.RBNode.IsCut.congr Batteries.RBNode.IsStrictCut.toIsCut
memP_iff_findP? 📖	mathematical	—	MemP findP?	—	Batteries.RBNode.Ordered.memP_iff_find? Batteries.RBNode.WF.out
memP_iff_lowerBoundP? 📖	mathematical	—	MemP lowerBoundP?	—	Batteries.RBNode.Ordered.memP_iff_lowerBound? Batteries.RBNode.WF.out
memP_iff_upperBoundP? 📖	mathematical	—	MemP upperBoundP?	—	Batteries.RBNode.Ordered.memP_iff_upperBound? Batteries.RBNode.WF.out
mem_congr 📖	mathematical	—	Batteries.RBSet instMembership	—	Batteries.RBNode.mem_congr
mem_iff_find? 📖	mathematical	—	Batteries.RBSet instMembership find?	—	memP_iff_findP? Batteries.RBNode.IsStrictCut.toIsCut Batteries.RBNode.instIsStrictCut
mem_iff_lowerBound? 📖	mathematical	—	Batteries.RBSet instMembership lowerBound?	—	memP_iff_lowerBoundP? Batteries.RBNode.IsStrictCut.toIsCut Batteries.RBNode.instIsStrictCut
mem_iff_mem_toList 📖	mathematical	—	Batteries.RBSet instMembership toList	—	Batteries.RBNode.mem_def
mem_iff_upperBound? 📖	mathematical	—	Batteries.RBSet instMembership upperBound?	—	memP_iff_upperBoundP? Batteries.RBNode.IsStrictCut.toIsCut Batteries.RBNode.instIsStrictCut
mem_insert 📖	mathematical	—	Batteries.RBSet instMembership insert	—	mem_iff_mem_toList mem_toList_insert mem_insert_of_mem mem_insert_of_eq
mem_insert_of_eq 📖	mathematical	—	Batteries.RBSet instMembership insert	—	mem_congr mem_insert_self
mem_insert_of_mem 📖	mathematical	Batteries.RBSet instMembership	insert	—	mem_iff_mem_toList mem_congr mem_insert_of_mem_toList
mem_insert_of_mem_toList 📖	mathematical	toList	Batteries.RBSet instMembership insert	—	mem_toList_insert_of_mem mem_of_mem_toList mem_iff_mem_toList mem_toList_insert_self
mem_insert_self 📖	mathematical	—	Batteries.RBSet instMembership insert	—	mem_of_mem_toList mem_toList_insert_self
mem_of_mem_toList 📖	mathematical	toList	Batteries.RBSet instMembership	—	mem_iff_mem_toList
mem_toList 📖	mathematical	—	toList Batteries.RBNode Batteries.RBNode.instMembership Batteries.RBNode.WF	—	Batteries.RBNode.mem_toList
mem_toList_insert 📖	mathematical	—	toList insert	—	Batteries.RBNode.WF.out Batteries.RBNode.mem_insert
mem_toList_insert_of_mem 📖	mathematical	toList	insert	—	Batteries.RBNode.WF.out mem_toList Batteries.RBNode.mem_insert_of_mem
mem_toList_insert_self 📖	mathematical	—	toList insert	—	Batteries.RBNode.WF.out mem_toList Batteries.RBNode.mem_insert_self
mem_toList_unique 📖	—	toList	—	—	Batteries.RBNode.Ordered.unique Batteries.RBNode.WF.out mem_toList
mkRBSet_eq 📖	mathematical	—	Batteries.mkRBSet Batteries.RBSet instEmptyCollection	—	—
single_toList 📖	mathematical	—	toList single	—	—
size_eq 📖	mathematical	—	size toList	—	Batteries.RBNode.size_eq
toList_sorted 📖	mathematical	—	Batteries.RBNode.cmpLT toList	—	Batteries.RBNode.Ordered.toList_sorted Batteries.RBNode.WF.out
toStream_eq 📖	mathematical	—	Batteries.RBSet Batteries.RBNode.Stream instToStreamStream Batteries.RBNode.toStream Batteries.RBNode Batteries.RBNode.WF Batteries.RBNode.Stream.nil	—	—
toStream_toList 📖	mathematical	—	Batteries.RBNode.Stream.toList Batteries.RBSet Batteries.RBNode.Stream instToStreamStream toList	—	Batteries.RBNode.toStream_toList
upperBound?_eq_find? 📖	mathematical	find?	upperBound?	—	upperBoundP?_eq_findP?
upperBound?_exists 📖	mathematical	—	upperBound? Batteries.RBSet instMembership	—	upperBoundP?_exists Batteries.RBNode.IsStrictCut.toIsCut Batteries.RBNode.instIsStrictCut
upperBound?_ge 📖	—	upperBound?	—	—	upperBoundP?_ge
upperBound?_mem 📖	mathematical	upperBound?	Batteries.RBSet instMembership	—	upperBoundP?_mem
upperBound?_mem_toList 📖	mathematical	upperBound?	toList	—	upperBoundP?_mem_toList
upperBoundP?_eq_findP? 📖	mathematical	findP?	upperBoundP?	—	Batteries.RBNode.upperBound?_eq_find?
upperBoundP?_exists 📖	mathematical	—	upperBoundP? Batteries.RBSet instMembership	—	Batteries.RBNode.Ordered.upperBound?_exists Batteries.RBNode.WF.out Batteries.RBNode.IsCut.congr
upperBoundP?_ge 📖	—	upperBoundP?	—	—	Batteries.RBNode.upperBound?_ge
upperBoundP?_least 📖	—	upperBoundP? Batteries.RBSet instMembership	—	—	mem_iff_mem_toList Batteries.RBNode.Ordered.upperBound?_least Batteries.RBNode.WF.out mem_toList Batteries.RBNode.IsCut.congr
upperBoundP?_mem 📖	mathematical	upperBoundP?	Batteries.RBSet instMembership	—	mem_of_mem_toList upperBoundP?_mem_toList
upperBoundP?_mem_toList 📖	mathematical	upperBoundP?	toList	—	mem_toList Batteries.RBNode.upperBound?_mem
val_toList 📖	mathematical	—	Batteries.RBNode.toList Batteries.RBNode Batteries.RBNode.WF toList	—	—

---

← Back to Index