cons_support — Mathlib

English

The support of s.cons y is contained in insert 0 and the image of s.support under Fin.succEmb.

Русский

Опора (support) s.cons y ⊆ вставка 0 ∪ образ support s под Fin.succEmb.

LaTeX

$$$(s.cons\\ y).\\text{support} \\subseteq \\text{insert } 0 \\ (\\text{map } (\\text{Fin.succEmb } n)\\ s.\\text{support})$$$

Lean4

theorem cons_support : (s.cons y).support ⊆ insert 0 (s.support.map (Fin.succEmb n)) :=
  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

Похожие утверждения