Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems `symm`, `arr_empty`, `arr_link`, `arr_push`, `equiv_empty`, `equiv_find`, `equiv_link`, `equiv_push`, `equiv_rootD`, `equiv_rootD_l`, `equiv_rootD_r`, `equiv_union`, `parentD_linkAux`, `parentD_push`, `parent_empty`, `parent_link`, `parent_push`, `rankD_push`, `rankMax_push`, `rank_empty`, `rank_push`, `rootD_empty`, `root_link`, `root_push`	24
Total	24

Batteries.UnionFind

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arr_empty` 📖	mathematical	—	`arr` `empty` `Batteries.UFNode`	—	—
`arr_link` 📖	mathematical	`parent` `size`	`arr` `link` `linkAux`	—	—
`arr_push` 📖	mathematical	—	`arr` `push` `Batteries.UFNode`	—	—
`equiv_empty` 📖	mathematical	—	`Equiv` `empty`	—	—
`equiv_find` 📖	mathematical	—	`Equiv` `Batteries.UnionFind` `size` `find`	—	`find_root_1`
`equiv_link` 📖	mathematical	`parent` `size`	`Equiv` `link`	—	`root_link` `rootD_eq_self`
`equiv_push` 📖	mathematical	—	`Equiv` `push`	—	`root_push`
`equiv_rootD` 📖	mathematical	—	`Equiv` `rootD`	—	`rootD_rootD`
`equiv_rootD_l` 📖	mathematical	—	`Equiv` `rootD`	—	`rootD_rootD`
`equiv_rootD_r` 📖	mathematical	—	`Equiv` `rootD`	—	`rootD_rootD`
`equiv_union` 📖	mathematical	—	`Equiv` `union` `size`	—	`find_root_2` `link.congr_simp` `equiv_link` `find_root_1` `rootD_rootD`
`parentD_linkAux` 📖	mathematical	—	`parentD` `linkAux` `Batteries.UFNode` `Batteries.UFNode.rank`	—	`parentD_set` `parentD_eq`
`parentD_push` 📖	mathematical	—	`parentD` `Batteries.UFNode`	—	—
`parent_empty` 📖	mathematical	—	`parent` `empty`	—	—
`parent_link` 📖	mathematical	`parent` `size`	`link` `rank`	—	`rankD_eq` `parentD_linkAux`
`parent_push` 📖	mathematical	—	`parent` `push`	—	`parentD_push`
`rankD_push` 📖	mathematical	—	`rankD` `Batteries.UFNode`	—	—
`rankMax_push` 📖	mathematical	—	`rankMax` `push`	—	—
`rank_empty` 📖	mathematical	—	`rank` `empty`	—	—
`rank_push` 📖	mathematical	—	`rank` `push`	—	`rankD_push`
`rootD_empty` 📖	mathematical	—	`rootD` `empty`	—	—
`root_link` 📖	mathematical	`parent` `size`	`rootD` `link`	—	`rootD_ext` `parent_link`
`root_push` 📖	mathematical	—	`rootD` `push`	—	`rootD_ext` `parent_push`

Batteries.UnionFind.Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`symm` 📖	—	`Batteries.UnionFind.Equiv`	—	—	—

---

← Back to Index