restrict_apply — Mathlib

English

Applying the restricted linear map yields the same as applying the original to the underlying value.

Русский

Применение ограниченного линейного отображения даёт то же, что и применение исходного к базовому значению.

LaTeX

$$$f.restrict hf x = f x$$$

Lean4

theorem restrict_apply {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) (x : p) :
    f.restrict hf x = ⟨f x, hf x.1 x.2⟩ :=
  rfl

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