mem_sup_support_iff — Mathlib

English

For a finite set s of finsupps, x belongs to the supremum of supports iff there exists a member f of s with x in its support.

Русский

Для конечного множества s финспп x принадлежит максимуму опор тогда и только тогда, когда существует f ∈ s с x ∈ opra f.

LaTeX

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

Lean4

theorem mem_sup_support_iff [Zero M] {s : Finset (ι →₀ M)} {x : ι} :
    x ∈ s.sup Finsupp.support ↔ ∃ f ∈ s, x ∈ f.support :=
  Multiset.mem_sup_map_support_iff

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