instLargeCategory

Mathlib.Topology.Category.UniformSpace

URI: https://scilib.ai/kg/mathlib#UniformSpaceCat.instLargeCategory

Lean4

instance : LargeCategory.{u} UniformSpaceCat.{u} where
  Hom := Hom
  id X := ⟨id, uniformContinuous_id⟩
  comp f g := ⟨⟨g.hom'.val ∘ f.hom'.val, g.hom'.property.comp f.hom'.property⟩⟩
  id_comp := by intros; apply Hom.ext; simp
  comp_id := by intros; apply Hom.ext; simp
  assoc := by intros; apply Hom.ext; ext; simp

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

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

Разделы

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

Аффилиация

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