subtype_comp_restrict — Mathlib

English

Let f be a linear map M → M₁ and p ⊆ M, q ⊆ M₁ with f(p) ⊆ q. Then restricting f to p and then embedding into q equals the domain restriction of f to p.

Русский

Пусть f: M → M₁ линейно, p ⊆ M и q ⊆ M₁ удовлетворяют f(p) ⊆ q. Тогда ограничение f до p и затем вложение в q равно ограничению области f на p.

LaTeX

$$$(\\forall x\\in p,\; f(x) \\in q) \\Rightarrow q.\\mathrm{subtype} \\circ (f|_p) = f|_p \\text{ as maps } p \\to M₁.$$$

Lean4

theorem subtype_comp_restrict {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) :
    q.subtype.comp (f.restrict hf) = f.domRestrict p :=
  rfl

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