Basic

📁 Source: Batteries/Data/UnionFind/Basic.lean

Statistics

Metric	Count
Definitions UFNode, parent, rank, Equiv, FindAux, root, s, arr, checkEquiv, checkEquiv!, checkEquivD, checkEquivN, empty, find, find!, findAux, findD, findN, instEmptyCollection, link, link!, linkAux, linkN, mkEmpty, parent, parentD, push, rank, rankD, rankMax, root, root!, rootD, rootN, size, union, union!, unionN	38
Theorems size_eq, findAux_root, findAux_s, find_parent_1, find_parent_or, find_root_1, find_root_2, find_size, le_rank_root, linkAux_size, lt_of_parentD, lt_rankD_findAux, lt_rankMax, lt_rank_root, parent'_lt, parentD_eq, parentD_findAux, parentD_findAux_lt, parentD_findAux_or, parentD_findAux_rootD, parentD_lt, parentD_of_not_lt, parentD_set, parent_lt, parent_root, parent_rootD, push_parentD, push_rankD, rank'_lt, rank'_lt_rankMax, rankD_eq, rankD_findAux, rankD_lt, rankD_lt_rankMax, rankD_set, rank_lt, rootD_eq_self, rootD_ext, rootD_lt, rootD_parent, rootD_rootD, setParentBump_rankD_lt, setParent_rankD_lt	43
Total	81

Batteries

Definitions

Name	Category	Theorems
UFNode 📖	CompData	13 math math: UnionFind.parent_root, UnionFind.findAux_s, UnionFind.parentD_findAux, UnionFind.linkAux_size, UnionFind.push_rankD, UnionFind.lt_of_parentD, UnionFind.parentD_push, UnionFind.push_parentD, UnionFind.FindAux.size_eq, UnionFind.arr_push, UnionFind.parentD_linkAux, UnionFind.rankD_push, UnionFind.arr_empty

Batteries.UFNode

Definitions

Name	Category	Theorems
parent 📖	CompOp	7 math math: Batteries.UnionFind.parentD_set, Batteries.UnionFind.rank'_lt, Batteries.UnionFind.parent_root, Batteries.UnionFind.findAux_s, Batteries.UnionFind.parentD_findAux, Batteries.UnionFind.parentD_eq, Batteries.UnionFind.parent'_lt
rank 📖	CompOp	5 math math: Batteries.UnionFind.rankD_set, Batteries.UnionFind.rankD_eq, Batteries.UnionFind.rank'_lt_rankMax, Batteries.UnionFind.findAux_s, Batteries.UnionFind.parentD_linkAux

Batteries.UnionFind

Definitions

Name	Category	Theorems
Equiv 📖	MathDef	9 math math: equiv_rootD_l, Equiv.rfl, equiv_rootD_r, equiv_push, equiv_empty, equiv_link, equiv_find, equiv_union, equiv_rootD
FindAux 📖	CompData	—
arr 📖	CompOp	8 math math: parent_root, findAux_s, parentD_findAux, arr_link, rankD_lt_rankMax, rankD_lt, arr_push, arr_empty
checkEquiv 📖	CompOp	—
checkEquiv! 📖	CompOp	—
checkEquivD 📖	CompOp	—
checkEquivN 📖	CompOp	—
empty 📖	CompOp	5 math math: rank_empty, equiv_empty, rootD_empty, parent_empty, arr_empty
find 📖	CompOp	6 math math: find_root_1, find_size, equiv_find, find_parent_or, find_root_2, find_parent_1
find! 📖	CompOp	—
findAux 📖	CompOp	8 math math: parentD_findAux_lt, parentD_findAux_or, findAux_root, lt_rankD_findAux, findAux_s, parentD_findAux, rankD_findAux, parentD_findAux_rootD
findD 📖	CompOp	—
findN 📖	CompOp	—
instEmptyCollection 📖	CompOp	—
link 📖	CompOp	4 math math: parent_link, arr_link, root_link, equiv_link
link! 📖	CompOp	—
linkAux 📖	CompOp	3 math math: linkAux_size, arr_link, parentD_linkAux
linkN 📖	CompOp	—
mkEmpty 📖	CompOp	—
parent 📖	CompOp	10 math math: rank_lt, parentD_findAux_or, parent_lt, parent_rootD, rootD_eq_self, find_parent_or, parent_push, rootD_parent, find_parent_1, parent_empty
parentD 📖	CompOp	13 math math: parentD_set, parentD_findAux_lt, parentD_findAux_or, lt_rankD_findAux, parentD_of_not_lt, parentD_findAux, parentD_findAux_rootD, parentD_eq, parentD_lt, parentD_push, rankD_lt, push_parentD, parentD_linkAux
push 📖	CompOp	6 math math: root_push, rank_push, equiv_push, rankMax_push, parent_push, arr_push
rank 📖	CompOp	10 math math: rank_lt, rank'_lt, parent_link, le_rank_root, rank_push, lt_rankD_findAux, rankD_findAux, lt_rank_root, rank_empty, lt_rankMax
rankD 📖	CompOp	7 math math: rankD_set, rankD_eq, rankD_findAux, push_rankD, rankD_lt_rankMax, rankD_lt, rankD_push
rankMax 📖	CompOp	4 math math: rank'_lt_rankMax, rankD_lt_rankMax, rankMax_push, lt_rankMax
root 📖	CompOp	2 math math: parent_root, findAux_root
root! 📖	CompOp	—
rootD 📖	CompOp	22 math math: parentD_findAux_or, equiv_rootD_l, le_rank_root, root_push, rootD_rootD, findAux_s, parentD_findAux, parentD_findAux_rootD, find_root_1, lt_rank_root, root_link, rootD_lt, parent_rootD, equiv_rootD_r, rootD_ext, rootD_eq_self, find_parent_or, find_root_2, rootD_empty, rootD_parent, find_parent_1, equiv_rootD
rootN 📖	CompOp	—
size 📖	CompOp	18 math math: parentD_findAux_or, parent_root, findAux_root, lt_rankD_findAux, findAux_s, parent_lt, parentD_findAux, rankD_findAux, parentD_findAux_rootD, find_root_1, find_size, rootD_lt, parent'_lt, equiv_find, find_parent_or, find_root_2, equiv_union, find_parent_1
union 📖	CompOp	1 math math: equiv_union
union! 📖	CompOp	—
unionN 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
findAux_root 📖	mathematical	—	FindAux.root size findAux root	—	findAux.eq_1 root.eq_1 FindAux.size_eq lt_rankMax rank'_lt
findAux_s 📖	mathematical	—	FindAux.s size findAux Batteries.UFNode Batteries.UFNode.parent arr parent'_lt rootD Batteries.UFNode.rank	—	parent'_lt rootD_parent parent.eq_1 parentD_eq findAux_root findAux.eq_1
find_parent_1 📖	mathematical	—	parent Batteries.UnionFind size find rootD	—	parent'_lt parentD_findAux
find_parent_or 📖	mathematical	—	parent Batteries.UnionFind size find rootD	—	parentD_findAux_or
find_root_1 📖	mathematical	—	rootD Batteries.UnionFind size find	—	rootD_eq_self find_parent_or lt_rankMax rank_lt rootD_parent rootD_rootD
find_root_2 📖	mathematical	—	size Batteries.UnionFind find rootD	—	findAux_root
find_size 📖	mathematical	—	size Batteries.UnionFind find	—	FindAux.size_eq
le_rank_root 📖	mathematical	—	rank rootD	—	rootD_eq_self lt_rankMax rank_lt rootD_parent
linkAux_size 📖	mathematical	—	Batteries.UFNode linkAux	—	—
lt_of_parentD 📖	mathematical	—	Batteries.UFNode	—	parentD_of_not_lt
lt_rankD_findAux 📖	mathematical	—	rank parentD FindAux.s size findAux	—	parent'_lt findAux_s rank_lt parentD_findAux lt_rankMax rank'_lt lt_rank_root rootD_eq_self
lt_rankMax 📖	mathematical	—	rank rankMax	—	rankD_lt_rankMax
lt_rank_root 📖	mathematical	—	rank rootD	—	rootD_eq_self rootD_parent rank_lt le_rank_root
parent'_lt 📖	mathematical	Batteries.UFNode arr	Batteries.UFNode.parent size	—	—
parentD_eq 📖	mathematical	Batteries.UFNode	parentD Batteries.UFNode.parent	—	—
parentD_findAux 📖	mathematical	—	parentD FindAux.s size findAux rootD Batteries.UFNode.parent Batteries.UFNode arr parent'_lt	—	parent'_lt findAux_s parentD.eq_1 FindAux.size_eq rootD_eq_self parentD_eq
parentD_findAux_lt 📖	mathematical	size	parentD FindAux.s findAux	—	—
parentD_findAux_or 📖	mathematical	—	parentD FindAux.s size findAux rootD parent	—	—
parentD_findAux_rootD 📖	mathematical	—	parentD FindAux.s size findAux rootD	—	parent'_lt parentD_findAux lt_rankMax rank'_lt parentD_eq parent.eq_1 rootD_eq_self rootD_parent
parentD_lt 📖	mathematical	Batteries.UFNode arr	parentD	—	—
parentD_of_not_lt 📖	mathematical	Batteries.UFNode	parentD	—	—
parentD_set 📖	mathematical	Batteries.UFNode	parentD Batteries.UFNode.parent	—	parentD.eq_1
parent_lt 📖	mathematical	—	parent size	—	—
parent_root 📖	mathematical	—	Batteries.UFNode.parent Batteries.UFNode arr size root	—	root.eq_1 lt_rankMax rank'_lt
parent_rootD 📖	mathematical	—	parent rootD	—	rootD.eq_1 parentD_of_not_lt parent_root
push_parentD 📖	mathematical	—	parentD Batteries.UFNode	—	—
push_rankD 📖	mathematical	—	rankD Batteries.UFNode	—	—
rank'_lt 📖	mathematical	Batteries.UFNode arr	rank Batteries.UFNode.parent	—	rankD_lt
rank'_lt_rankMax 📖	mathematical	Batteries.UFNode arr	Batteries.UFNode.rank rankMax	—	—
rankD_eq 📖	mathematical	Batteries.UFNode	rankD Batteries.UFNode.rank	—	—
rankD_findAux 📖	mathematical	—	rankD FindAux.s size findAux rank	—	—
rankD_lt 📖	mathematical	—	rankD arr parentD	—	—
rankD_lt_rankMax 📖	mathematical	—	rankD arr rankMax	—	rank'_lt_rankMax
rankD_set 📖	mathematical	Batteries.UFNode	rankD Batteries.UFNode.rank	—	rankD.eq_1
rank_lt 📖	mathematical	—	rank parent	—	rankD_lt
rootD_eq_self 📖	mathematical	—	rootD parent	—	parent_rootD rootD.eq_1 root.eq_1 parentD_eq parent.eq_1
rootD_ext 📖	mathematical	parent	rootD	—	rootD_eq_self lt_rankMax rank_lt rootD_parent
rootD_lt 📖	mathematical	—	rootD size	—	—
rootD_parent 📖	mathematical	—	rootD parent	—	parentD_of_not_lt root.eq_1
rootD_rootD 📖	mathematical	—	rootD	—	rootD_eq_self parent_rootD
setParentBump_rankD_lt 📖	—	Batteries.UFNode.rank Batteries.UFNode Batteries.UFNode.parent rankD parentD	—	—	rankD_eq parentD_eq
setParent_rankD_lt 📖	—	Batteries.UFNode.rank Batteries.UFNode rankD parentD	—	—	setParentBump_rankD_lt parentD_set rankD_set rankD_eq

Batteries.UnionFind.FindAux

Definitions

Name	Category	Theorems
root 📖	CompOp	1 math math: Batteries.UnionFind.findAux_root
s 📖	CompOp	8 math math: Batteries.UnionFind.parentD_findAux_lt, Batteries.UnionFind.parentD_findAux_or, Batteries.UnionFind.lt_rankD_findAux, Batteries.UnionFind.findAux_s, Batteries.UnionFind.parentD_findAux, Batteries.UnionFind.rankD_findAux, Batteries.UnionFind.parentD_findAux_rootD, size_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
size_eq 📖	mathematical	—	Batteries.UFNode s	—	—

---

← Back to Index