map_subtype_range_inclusion

Mathlib.Algebra.Module.Submodule.Range

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

← MathLib Explorer

English

The image of the inclusion map from p to q equals p when p ≤ q.

Русский

Образ включения p в q равен p, если p ⊆ q.

LaTeX

$$$$ \operatorname{map}(p.\mathrm{subtype}, \operatorname{range}(\mathrm{inclusion}(h))) = p $$$$

Lean4

@[simp]
theorem map_subtype_range_inclusion {p p' : Submodule R M} (h : p ≤ p') : map p'.subtype (range <| inclusion h) = p :=
  by simp [range_inclusion, map_comap_eq, h]

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

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

Разделы

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

Аффилиация

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