map_subtype_le

Mathlib.Algebra.Module.Submodule.Range

URI: https://scilib.ai/kg/mathlib#Submodule.map_subtype_le

English

For every p' ⊆ p, the image of p' under the inclusion into M is contained in p.

Русский

Для любого p' ⊆ p образ p' через включение в M лежит в p.

LaTeX

$$$$ \operatorname{map}(p.\mathrm{subtype}, p') \le p $$$$

Lean4

theorem map_subtype_le (p' : Submodule R p) : map p.subtype p' ≤ p := by
  simpa using (map_le_range : map p.subtype p' ≤ range p.subtype)

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

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

Разделы

Аффилиация

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