inclusionSpan — Mathlib

English

The span of the range of the inclusion map is the whole space, i.e., top.

Русский

Покрытие пространства спаном диапазона включения — это вся область.

LaTeX

$$$\operatorname{span}_S(\operatorname{range}(\operatorname{inclusion} \; p)) = \top$$$

Lean4

/-- The inclusion of an `R`-submodule into its `S`-span, as an `R`-linear map. -/
@[simps]
def inclusionSpan : p →ₗ[R] span S (p : Set M)
    where
  toFun x := ⟨x, subset_span x.property⟩
  map_add' x y := by simp
  map_smul' t x := by simp

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