mem_sup_map_support_iff — Mathlib

English

For a multiset s of finsupps, an element x lies in the supremum of mapped supports iff there exists f in s with x in f.support.

Русский

Для мультимножества s финспп x принадлежит максимуму (sup) опор, эквивалентно существованию элемента f в s с x в опоре f.

LaTeX

$$$x \\\\in (s.map Finsupp.\\\\operatorname{support}).\\\\sup \\\\iff \\\\exists f \\\\in s, x \\\\in f.\\\\operatorname{support}$$$

Lean4

theorem mem_sup_map_support_iff [Zero M] {s : Multiset (ι →₀ M)} {x : ι} :
    x ∈ (s.map Finsupp.support).sup ↔ ∃ f ∈ s, x ∈ f.support :=
  Quot.inductionOn s fun _ ↦ by
    simpa only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sup_coe, List.foldr_map] using
      List.mem_foldr_sup_support_iff

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