UnionFind.model'
theorem UnionFind.model' : ∀ {α : Type u_1} (self : UnionFind α), ∃ m, UFModel.Models self.arr m
The theorem `UnionFind.model'` states that for any type `α` and any object `self` of the type `UnionFind α`, there exists a model `m` such that `m` models the array `self.arr` according to the function `UFModel.Models`. In other words, it asserts that every instance of a `UnionFind` structure can be modeled by some `UFModel`, where the model agrees with the `UnionFind` structure's array in terms of parent and rank attributes.
More concisely: For any type `α` and `UnionFind` object `self` over `α`, there exists a `UFModel` `m` such that `self.arr` and `m` agree on parent and rank attributes.
|
UFModel.Models.size_eq
theorem UFModel.Models.size_eq :
∀ {α : Type u_1} {arr : Array (UFNode α)} {n : ℕ} {m : UFModel n}, UFModel.Models arr m → n = arr.size
The theorem `UFModel.Models.size_eq` states that for any type `α`, any array `arr` of Union-Find Nodes (`UFNode α`), any natural number `n`, and any Union-Find model `m` of size `n`, if the array `arr` models the Union-Find model `m` (as specified by the `UFModel.Models` function), then `n` is equal to the size of the array `arr` (`Array.size arr`). Essentially, this theorem is asserting that the size of the Union-Find model and the size of the array that models it are always equal.
More concisely: For any Union-Find model `m` of size `n` and any array `arr` of `UFNode α` that models `m`, we have `n = Array.size arr`.
|
UFModel.Agrees.get_eq
theorem UFModel.Agrees.get_eq :
∀ {α : Type u_1} {β : Sort u_2} {f : α → β} {arr : Array α} {n : ℕ} {m : Fin n → β},
UFModel.Agrees arr f m → ∀ (i : ℕ) (h₁ : i < arr.size) (h₂ : i < n), f (arr.get ⟨i, h₁⟩) = m ⟨i, h₂⟩
This theorem states that if there is an agreement between an array `arr` of type α, a function `f` mapping α to β, and another function `m` mapping indices to β, then for every index `i` that is less than the size of the array and less than `n`, applying the function `f` to the element in the array at index `i` will yield the same result as applying the function `m` to the index `i`. This agreement is denoted by `UFModel.Agrees arr f m` in the theorem.
More concisely: For any array `arr` of type α, function `f` from α to β, and function `m` mapping indices to β, if `UFModel.Agrees arr f m` holds, then `f arr i = m i` for all indices `i` less than the array size.
|
UFModel.Models.rank_eq
theorem UFModel.Models.rank_eq :
∀ {α : Type u_1} {arr : Array (UFNode α)} {n : ℕ} {m : UFModel n},
UFModel.Models arr m → ∀ (i : ℕ) (h : i < arr.size), arr[i].rank = m.rank i
This theorem, `UFModel.Models.rank_eq`, states that for any type `α`, any array of Union-Find nodes `arr` of type `UFNode α`, any natural number `n`, and any Union-Find model `m` of size `n`, if the array `arr` models the Union-Find model `m` (as per the definition of `UFModel.Models`), then for every natural number `i` that is less than the size of the array `arr`, the rank of the `i`-th node in the array `arr` is equal to the rank of the `i`-th node in the Union-Find model `m`.
In simpler terms, it states that if an array of Union-Find nodes correctly models a Union-Find model, then each node in the array and the corresponding node in the model must have the same rank.
More concisely: For any Union-Find model `m` of size `n` and any array `arr` of Union-Find nodes of type `UFNode α` modeling `m`, the rank of the `i`-th node in `arr` equals the rank of the `i`-th node in `m` for all `i` in the range `0` to `n-1`.
|
UFModel.Models.parent_eq
theorem UFModel.Models.parent_eq :
∀ {α : Type u_1} {arr : Array (UFNode α)} {n : ℕ} {m : UFModel n},
UFModel.Models arr m → ∀ (i : ℕ) (h₁ : i < arr.size) (h₂ : i < n), arr[i].parent = ↑(m.parent ⟨i, h₂⟩)
The theorem `UFModel.Models.parent_eq` states that for any type `α`, any array `arr` of `UFNode α`, any natural number `n`, and any `UFModel n` `m`, if `arr` models `m`, then for any natural number `i` such that `i` is less than the size of the array `arr` and `i` is less than `n`, the parent of the `i`-th element of `arr` is equal to the parent of the `i`-th element of `m`. This theorem essentially says that when a `UFModel` is modeled by an array of `UFNode`, the parent relationships within the array and the model are consistent.
More concisely: For any array `arr` of `UFNode` modeling `UFModel` `m`, and for all `i` less than the size of `arr` and `n`, the parent of the `i`-th element in `arr` equals the parent of the `i`-th element in `m`.
|