restrict_eq_codRestrict_domRestrict

English

If f maps p into q, then restricting f to p and viewing the result as a map into q coincides with the natural codomain restriction of f to q.

Русский

Если f отправляет p в q, то ограничение f до p и восприятие результата как отображение в q совпдает с естественным ограничением кодом отображения f до q.

LaTeX

$$$\\text{If } \\forall x\\in p,\\ f(x) \\in q,\\text{ then } f\\restriction p = q.\\text{codRestrict} \\; q \\; f \\; \\text{on } p.$$$

Lean4

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

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