apply_coe_mem_map — Mathlib

English

Let p be a submodule of M and f a semilinear map M →ₛₗ[σ] M₂. Then for every r in p, f(r) lies in the image of p under f, i.e., f(r) ∈ map f p.

Русский

Пусть p — подмодуль M, и f — полуприводоподобное линейное отображение M →ₛₗ[σ] M₂. Тогда для любого r ∈ p верно, что f(r) принадлежит образу p под действием f, то есть f(r) ∈ map f p.

LaTeX

$$$\\forall$ r ∈ p, f(r) \\in map f\,p$$

Lean4

theorem apply_coe_mem_map (f : F) {p : Submodule R M} (r : p) : f r ∈ map f p :=
  mem_map_of_mem r.prop

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