isQuotient_explicitCokernelπ

Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

URI: https://scilib.ai/kg/mathlib#SemiNormedGrp.isQuotient_explicitCokernelπ

← MathLib Explorer

English

IsQuotient of (explicitCokernelπ f).hom holds.

Русский

Утверждается, что (explicitCokernelπ f).hom образует фактор-мопицию.

LaTeX

$$$\\\\operatorname{IsQuotient}((\\\\mathrm{explicitCokernel\\\\pi} f).\\\\mathrm{hom}).$$$

Lean4

theorem isQuotient_explicitCokernelπ {X Y : SemiNormedGrp.{u}} (f : X ⟶ Y) :
    NormedAddGroupHom.IsQuotient (explicitCokernelπ f).hom :=
  NormedAddGroupHom.isQuotientQuotient _

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

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

Разделы

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

Аффилиация

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