def Regex.Data.SparseSet.Bijection.inj {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

Equations

• Regex.Data.SparseSet.Bijection.inj f = ∀ (x y : α), f x = f y → x = y

def Regex.Data.SparseSet.Bijection.surj {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

Equations

• Regex.Data.SparseSet.Bijection.surj f = ∀ (y : β), ∃ (x : α), f x = y

def Regex.Data.SparseSet.Bijection.bij {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

Equations

• Regex.Data.SparseSet.Bijection.bij f = (Regex.Data.SparseSet.Bijection.inj f ∧ Regex.Data.SparseSet.Bijection.surj f)

theorem Fin.eq_of_ge {n : Nat} {i : Fin (n + 1)} (h : ↑i ≥ n) : i = ⟨n, ⋯⟩

theorem Fin.eq_of_not_lt {n : Nat} {i : Fin (n + 1)} (h : ¬↑i < n) : i = ⟨n, ⋯⟩

theorem Regex.Data.SparseSet.Bijection.surj_of_inj {n : Nat} (f : Fin n → Fin n) (h : inj f) : surj f