English
If s and t are disjoint subsets of α, then the submodules generated by the ranges of lsingle over s and over t are disjoint.
Русский
Если s и t — непересекающиеся подмножества α, то подпространства, порождаемые образами lsingle над s и над t, взаимно дизъюнктны.
LaTeX
$$$\operatorname{Disjoint}\left( \bigvee_{a\in s} \operatorname{range}(\mathrm{lsingle} a), \bigvee_{a\in t} \operatorname{range}(\mathrm{lsingle} a) \right)$$$
Lean4
theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) :
Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M))
(⨆ a ∈ t, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) :=
by
refine
(Disjoint.mono (lsingle_range_le_ker_lapply s sᶜ disjoint_compl_right)
(lsingle_range_le_ker_lapply t tᶜ disjoint_compl_right))
?_
rw [disjoint_iff_inf_le]
refine le_trans (le_iInf fun i => ?_) iInf_ker_lapply_le_bot
classical
by_cases his : i ∈ s
· by_cases hit : i ∈ t
· exact (hs.le_bot ⟨his, hit⟩).elim
exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)
exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)
