English
For a family of sets s_i, the supported submodule on the union equals the iSup of the supports.
Русский
Для семейства множеств $s_i$ поддерживаемый подмодуль на объединении равен объединению по отношению к iSup.
LaTeX
$$$\mathrm{supported}(M,R,\bigcup_i s_i) = \bigvee_i \mathrm{supported}(M,R,s_i)$$$
Lean4
theorem supported_iUnion {δ : Type*} (s : δ → Set α) : supported M R (⋃ i, s i) = ⨆ i, supported M R (s i) :=
by
refine le_antisymm ?_ (iSup_le fun i => supported_mono <| Set.subset_iUnion _ _)
haveI := Classical.decPred fun x => x ∈ ⋃ i, s i
suffices LinearMap.range ((Submodule.subtype _).comp (restrictDom M R (⋃ i, s i))) ≤ ⨆ i, supported M R (s i) by
rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
rw [range_le_iff_comap, eq_top_iff]
rintro l ⟨⟩
induction l using Finsupp.induction with
| zero => exact zero_mem _
| single_add x a l _ _ ih =>
refine add_mem ?_ ih
by_cases h : ∃ i, x ∈ s i
· simp only [mem_comap, coe_comp, coe_subtype, Function.comp_apply, restrictDom_apply, mem_iUnion, h,
filter_single_of_pos]
obtain ⟨i, hi⟩ := h
exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi)
· simp [h]
