chore(Data/Finsupp/Fin): add Finsupp.cons_support (#10192)

leanprover-community · Feb 9, 2024 · 555effe · 555effe
1 parent 9860584
commit 555effe
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean
@@ -92,4 +92,11 @@ theorem cons_ne_zero_iff : cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0 := by
   rw [h', c, Finsupp.cons_zero_zero]
 #align finsupp.cons_ne_zero_iff Finsupp.cons_ne_zero_iff
 
+lemma cons_support : (s.cons y).support ⊆ insert 0 (s.support.map (Fin.succEmb n).toEmbedding) := by
+  intro i hi
+  suffices i = 0 ∨ ∃ a, ¬s a = 0 ∧ a.succ = i by simpa
+  apply (Fin.eq_zero_or_eq_succ i).imp id (Exists.imp _)
+  rintro i rfl
+  simpa [Finsupp.mem_support_iff] using hi
+
 end Finsupp