map₂_span_singleton_eq_map

Mathlib.Algebra.Module.Submodule.Bilinear

URI: https://scilib.ai/kg/mathlib#Submodule.map₂_span_singleton_eq_map

← MathLib Explorer

English

For any m, map₂ f (span{m}) equals the image map of f at m.

Русский

Для любого m отображение map₂ f на span{m} равно образу f на m.

LaTeX

$$map₂ f (span R { m }) = map (f m)$$

Lean4

theorem map₂_span_singleton_eq_map (f : M →ₗ[R] N →ₗ[R] P) (m : M) : map₂ f (span R { m }) = map (f m) :=
  by
  funext s
  rw [← span_eq s, map₂_span_span, image2_singleton_left, map_span]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru