@[simp]
@[simp]
@[simp]
@[simp]
theorem
Batteries.UnionFind.arr_link
{self : UnionFind}
{x y : Fin self.size}
{yroot : self.parent ↑y = ↑y}
:
theorem
Batteries.UnionFind.parent_link
{self : UnionFind}
{x y : Fin self.size}
(yroot : self.parent ↑y = ↑y)
{i : Nat}
:
@[simp]
@[simp]
@[simp]
theorem
Batteries.UnionFind.equiv_link
{a b : Nat}
{self : UnionFind}
{x y : Fin self.size}
(xroot : self.parent ↑x = ↑x)
(yroot : self.parent ↑y = ↑y)
: