comap_subtype_self

Mathlib.Algebra.Module.Submodule.Range

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

English

Comap of p.subtype with p equals top.

Русский

Комап по включению p.subtype с p равен верхнему подмодулю.

LaTeX

$$$$ \operatorname{comap}(p.\mathrm{subtype}, p) = \top $$$$

Lean4

@[simp]
theorem comap_subtype_self : comap p.subtype p = ⊤ :=
  comap_subtype_eq_top.2 le_rfl

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

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

Разделы

Аффилиация

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