fork

Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

URI: https://scilib.ai/kg/mathlib#SemiNormedGrp.fork

Lean4

/-- The equalizer cone for a parallel pair of morphisms of seminormed groups. -/
def fork {V W : SemiNormedGrp.{u}} (f g : V ⟶ W) : Fork f g :=
  @Fork.ofι _ _ _ _ _ _ (of (f - g).hom.ker) (ofHom (NormedAddGroupHom.incl (f - g).hom.ker)) <|
    by
    ext v
    have : v.1 ∈ (f - g).hom.ker := v.2
    simpa [-SetLike.coe_mem, NormedAddGroupHom.mem_ker, sub_eq_zero] using this

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

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

Разделы

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

Аффилиация

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