range_map — Mathlib

English

Range corresponds to the standard tensor-product construction from p and q.

Русский

Образ соответствует стандартной конструкции тензорного произведения из p и q.

LaTeX

$$$\\operatorname{range}(\\mathrm{mapIncl}\\ p\\ q) = \\mathrm{map_2}(\\mathrm{mk}\\ R\\ P\\ Q)\\ p\\ q$$$

Lean4

theorem range_map (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : range (map f g) = .map₂ (mk R _ _) (range f) (range g) :=
  by
  simp_rw [← Submodule.map_top, Submodule.map₂_map_map, ← map₂_mk_top_top_eq_top, Submodule.map_map₂]
  rfl

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