theorem Regex.Data.SparseSet.mem_insert_of_mem {n : Nat} {s : SparseSet n} {i j : Fin n} : i ∈ s → i ∈ s.insert j

theorem Regex.Data.SparseSet.eq_or_mem_of_mem_insert {n : Nat} {s : SparseSet n} {i j : Fin n} : i ∈ s.insert j → i = j ∨ i ∈ s

theorem Regex.Data.SparseSet.subset_self {n : Nat} {s : SparseSet n} : s ⊆ s

theorem Regex.Data.SparseSet.mem_of_mem_of_subset {n : Nat} {s₁ s₂ : SparseSet n} {i : Fin n} (mem : i ∈ s₁) (sub : s₁ ⊆ s₂) : i ∈ s₂

theorem Regex.Data.SparseSet.subset_insert {n : Nat} {i : Fin n} {s : SparseSet n} : s ⊆ s.insert i

theorem Regex.Data.SparseSet.subset_trans {n : Nat} {s₁ s₂ s₃ : SparseSet n} (h₁ : s₁ ⊆ s₂) (h₂ : s₂ ⊆ s₃) : s₁ ⊆ s₃

instance Regex.Data.SparseSet.instTransSubset_regexCorrectness {n : Nat} : Trans (fun (x1 x2 : SparseSet n) => x1 ⊆ x2) (fun (x1 x2 : SparseSet n) => x1 ⊆ x2) fun (x1 x2 : SparseSet n) => x1 ⊆ x2

Equations

• Regex.Data.SparseSet.instTransSubset_regexCorrectness = { trans := ⋯ }

theorem Regex.Data.SparseSet.mem_get {n : Nat} {s : SparseSet n} {i : Nat} (h : i < s.count) : s[i] ∈ s

def Regex.Data.SparseSet.index {n : Nat} (i : Fin n) (s : SparseSet n) : Nat

Equations

• Regex.Data.SparseSet.index i s = ↑s.sparse[i]

theorem Regex.Data.SparseSet.index_of_mem {n : Nat} {i : Fin n} {s : SparseSet n} (h : i ∈ s) : ∃ (x : index i s < s.count), s[index i s] = i