range_coeLinearMap — Mathlib

English

The range of the canonical linear map from the direct sum of submodules A_i equals the supremum (join) of the A_i inside M.

Русский

Область определения канонического линейного отображения прямой суммы подмодулов A_i равна сумме-объединению (объединению) всех A_i внутри M.

LaTeX

$$$\operatorname{range}(\mathrm{coeLinearMap} A) = \bigvee_i A_i.$$$

Lean4

theorem range_coeLinearMap : LinearMap.range (coeLinearMap A) = ⨆ i, A i :=
  (Submodule.iSup_eq_range_dfinsupp_lsum _).symm

Похожие утверждения