feat: some array lemma aliases (#891)

leanprover-community · Jul 30, 2024 · 3dfb59c · 3dfb59c
1 parent e789780
commit 3dfb59c
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
@@ -133,3 +133,15 @@ theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
   rw [mapM, mapM.map]; rfl
 
 @[simp] theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty ..
+
+/-! ### mem -/
+
+alias not_mem_empty := not_mem_nil
+
+theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
+
+/-! ### append -/
+
+alias append_empty := append_nil
+
+alias empty_append := nil_append