mem_iSup_iff_exists_dfinsupp — Mathlib

English

An element x lies in the supremum iSup S iff there exists a dfinsupp f with values in S_i such that the sumAddHom applied to f equals x.

Русский

Элемент x лежит в iSup S тогда и только тогда, когда существует dfinsupp f со значениями в S_i, для которого сумма через sumAddHom даёт x.

LaTeX

$$$ x \in \iSup S \iff \exists f:\Pi₀ i, S_i,\ \mathrm{sumAddHom}(\text{fun } i \mapsto (S_i).subtype) \, f = x$$$

Lean4

theorem mem_iSup_iff_exists_dfinsupp [AddCommMonoid γ] (S : ι → AddSubmonoid γ) (x : γ) :
    x ∈ iSup S ↔ ∃ f : Π₀ i, S i, DFinsupp.sumAddHom (fun i => (S i).subtype) f = x :=
  SetLike.ext_iff.mp (AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom S) x

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