restrict_coe_apply — Mathlib

English

The restriction map acts as f on the underlying elements when viewed on the subtype.

Русский

Ограниченное отображение действует как исходное отображение на элементе подмножества.

LaTeX

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

Lean4

@[simp]
theorem restrict_coe_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 :=
  rfl

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