English
If s and t are disjoint subsets of α, then the supremum of the ranges of lsingle over s is contained in the infimum of the kernels of lapply over t.
Русский
Пусть s и t — непересекающиеся множества подмножеств α. Тогда наибольшая верхняя грань множеств образов lsingle над s заключена в наименьшее верхнее множество ядер lapply над t.
LaTeX
$$$\bigvee_{a\in s} \operatorname{range}(\mathrm{lsingle} a) \le \bigwedge_{a\in t} \ker (\mathrm{lapply} a)$$$
Lean4
theorem lsingle_range_le_ker_lapply (s t : Set α) (h : Disjoint s t) :
⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M) ≤ ⨅ a ∈ t, ker (lapply a : (α →₀ M) →ₗ[R] M) :=
by
refine iSup_le fun a₁ => iSup_le fun h₁ => range_le_iff_comap.2 ?_
simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]
intro b _ a₂ h₂
have : a₂ ≠ a₁ := fun eq => h.le_bot ⟨h₁, eq.symm ▸ h₂⟩
exact single_eq_of_ne this
