English
For a finite index set s, membership in the iSup over i in s is equivalent to the existence of a finite sum representation by components μ_i ∈ p_i.
Русский
Для конечного множества индексов s принадлежность к iSup над i в s эквивалентна существованию представления суммы по компонентам μ_i ∈ p_i.
LaTeX
$$$(a ∈ \\bigl\\bowtie_{i \\in s} p_i\\bigr) \\iff \\exists \\mu, \\sum_{i \\in s} (\\mu_i) = a$$$
Lean4
theorem mem_iSup_finset_iff_exists_sum {s : Finset ι} (p : ι → Submodule R N) (a : N) :
(a ∈ ⨆ i ∈ s, p i) ↔ ∃ μ : ∀ i, p i, (∑ i ∈ s, (μ i : N)) = a := by
classical
rw [Submodule.mem_iSup_iff_exists_dfinsupp']
constructor <;> rintro ⟨μ, hμ⟩
· use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩
rw [← hμ]
symm
apply Finset.sum_subset
· intro x
contrapose
intro hx
rw [mem_support_iff, not_ne_iff]
ext
rw [coe_zero, ← mem_bot R]
suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
exact (iSup_neg hx).symm
· intro x _ hx
rw [mem_support_iff, not_ne_iff] at hx
rw [hx]
rfl
· refine ⟨DFinsupp.mk s ?_, ?_⟩
· rintro ⟨i, hi⟩
refine ⟨μ i, ?_⟩
rw [iSup_pos]
· exact coe_mem _
· exact hi
simp only [DFinsupp.sum]
rw [Finset.sum_subset support_mk_subset, ← hμ]
· exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]
· intro x _ hx
rw [mem_support_iff, not_ne_iff] at hx
rw [hx]
rfl
