mem_biSup_iff_exists_dfinsupp — Mathlib

English

Fully unfolded version of the iSup membership characterization via dfinsupp; expresses membership in iSup as existence of a dfinsupp with an equality.

Русский

Полная распаковка характеристика принадлежности iSup через dfinsupp; существует dfinsupp с равенством.

LaTeX

$$$x \\in iSup p' \\;\\iff\\; \\exists f : Π₀ i, p i, \\; (f.sum (..) ) = x$$$

Lean4

theorem mem_biSup_iff_exists_dfinsupp (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) (x : N) :
    (x ∈ ⨆ (i) (_ : p i), S i) ↔ ∃ f : Π₀ i, S i, DFinsupp.lsum ℕ (fun i => (S i).subtype) (f.filter p) = x :=
  SetLike.ext_iff.mp (biSup_eq_range_dfinsupp_lsum p S) x

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