English
If I and J are disjoint, then the ranges of singles over I and over J are disjoint submodules.
Русский
Если I и J дисъюнкты, то образы одиночных отображений по I и по J не пересекаются.
LaTeX
$$$\\text{Disjoint}\\; (\\,i\\;\\text{range}(\\text{single } i))\\; (\\,i\\;\\text{range}(\\text{single } i))$ with $I,J$ disjoint.$$
Lean4
theorem disjoint_single_single (I J : Set ι) (h : Disjoint I J) :
Disjoint (⨆ i ∈ I, range (single R φ i)) (⨆ i ∈ J, range (single R φ i)) :=
by
refine
Disjoint.mono (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right)
(iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right) ?_
simp only [disjoint_iff_inf_le, SetLike.le_def, mem_iInf, mem_inf, mem_ker, mem_bot, proj_apply, funext_iff]
rintro b ⟨hI, hJ⟩ i
classical
by_cases hiI : i ∈ I
· by_cases hiJ : i ∈ J
· exact (h.le_bot ⟨hiI, hiJ⟩).elim
· exact hJ i hiJ
· exact hI i hiI
