feat(data/list/pairwise): pairwise repeat (#11117)

leanprover-community · Dec 29, 2021 · cb37df3 · cb37df3
1 parent d8b4267
commit cb37df3
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/data/list/pairwise.lean b/src/data/list/pairwise.lean
@@ -330,6 +330,11 @@ theorem pairwise_sublists {R} {l : list α} (H : pairwise R l) :
 by have := pairwise_sublists' (pairwise_reverse.2 H);
    rwa [sublists'_reverse, pairwise_map] at this
 
+lemma pairwise_repeat {α : Type*} {r : α → α → Prop} {x : α} (hx : r x x) :
+  ∀ (n : ℕ), pairwise r (repeat x n)
+| 0 := by simp
+| (n+1) := by simp [hx, mem_repeat, pairwise_repeat n]
+
 /-! ### Pairwise filtering -/
 
 variable [decidable_rel R]