comap_map_mkQ

Mathlib.LinearAlgebra.Quotient.Basic

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

English

The comap of p.mkQ with the map p.mkQ p' equals p ⊔ p' (join).

Русский

Комап p.mkQ (map p.mkQ p') образует p ⊔ p'.

LaTeX

$$$$ \\operatorname{comap}_{p.mkQ} (\\operatorname{map}_{p.mkQ} p') = p \\lor p'. $$$$

Lean4

@[simp]
theorem comap_map_mkQ : comap p.mkQ (map p.mkQ p') = p ⊔ p' := by simp [comap_map_eq, sup_comm]

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

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

Разделы

Аффилиация

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