cokernelCocone

Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

URI: https://scilib.ai/kg/mathlib#SemiNormedGrp₁.cokernelCocone

Lean4

/-- Auxiliary definition for `HasCokernels SemiNormedGrp₁`. -/
def cokernelCocone {X Y : SemiNormedGrp₁.{u}} (f : X ⟶ Y) : Cofork f 0 :=
  Cofork.ofπ
    (@SemiNormedGrp₁.mkHom _ (Y ⧸ NormedAddGroupHom.range f.1) _ _ f.hom.1.range.normedMk
      (NormedAddGroupHom.isQuotientQuotient _).norm_le)
    (by
      ext x
      rw [Limits.zero_comp, comp_apply, SemiNormedGrp₁.mkHom_apply, SemiNormedGrp₁.zero_apply, ←
        NormedAddGroupHom.mem_ker, f.hom.1.range.ker_normedMk, f.hom.1.mem_range]
      use x)

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

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

Разделы

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

Аффилиация

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