restrict_eq_domRestrict_codRestrict

English

Let t be a finite index set and f_i: M →ₗ[σ] M₂ be linear maps. Then the sum map (∑ i∈t f_i) acts on b ∈ M by (∑ i∈t f_i)(b) = ∑ i∈t f_i(b).

Русский

Пусть t — конечный индексный набор и f_i: M →ₗ[σ] M₂ линейные отображения. Тогда сумма отображений применима к b так же, как сумма их значений: (∑ i∈t f_i)(b) = ∑ i∈t f_i(b).

LaTeX

$$$\\left(\\sum_{d\\in t} f_d\\right) b = \\sum_{d\\in t} (f_d b).$$$

Lean4

theorem restrict_eq_domRestrict_codRestrict {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁}
    (hf : ∀ x, f x ∈ q) : (f.restrict fun x _ => hf x) = (f.codRestrict q hf).domRestrict p :=
  rfl

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