instMonoFunctorOppositeTypeι_1

Mathlib.CategoryTheory.Subpresheaf.Equalizer

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.instMonoFunctorOppositeTypeι_1

English

The map equalizer.ι f g is mono.

Русский

Образ равнителя ι f g является моно.

LaTeX

$$$\\text{Mono}(\\text{equalizer.ι } f g)$$$

Lean4

instance : Mono (equalizer.ι f g) := by
  dsimp [equalizer.ι]
  infer_instance

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

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

Разделы

Аффилиация

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