instMonoOfLE

Mathlib.CategoryTheory.Subobject.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subobject.instMonoOfLE

← MathLib Explorer

English

If f ≫ Y.arrow = X.arrow then X ≤ Y.

Русский

Если f ≫ Y.arrow = X.arrow, то X ≤ Y.

LaTeX

$$$f \\;\\gg\\; Y.arrow = X.arrow \\Rightarrow X \\le Y$$$

Lean4

instance {B : C} (X Y : Subobject B) (h : X ≤ Y) : Mono (ofLE X Y h) :=
  by
  fconstructor
  intro Z f g w
  replace w := w =≫ Y.arrow
  ext
  simpa using w

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

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

Разделы

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

Аффилиация

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