mem_bsupr_iff_exists_dfinsupp — Mathlib

English

A bounded supremum membership lemma: x ∈ ⨆ i (p i), S i iff there exists a dfinsupp f with support filtered by p such that sumAddHom equals x.

Русский

Членство в ограниченном верхнем пределe: x ∈ ⨆ i, p i : S i тогда существует dfinsupp f с фильтрованной поддержкой, для которого сумма sumAddHom равна x.

LaTeX

$$(x ∈ ⨆ (i) (_ : p i), S i) ↔ ∃ f : Π₀ i, S i, DFinsupp.sumAddHom (fun i => (S i).subtype) (f.filter p) = x$$

Lean4

theorem mem_bsupr_iff_exists_dfinsupp (p : ι → Prop) [DecidablePred p] [AddCommMonoid γ] (S : ι → AddSubmonoid γ)
    (x : γ) :
    (x ∈ ⨆ (i) (_ : p i), S i) ↔ ∃ f : Π₀ i, S i, DFinsupp.sumAddHom (fun i => (S i).subtype) (f.filter p) = x :=
  SetLike.ext_iff.mp (AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom p S) x

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