mk_le_of_comm

Mathlib.CategoryTheory.Subobject.Basic

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

← MathLib Explorer

English

If there exists g: A1 → A2 with g ≫ f2 = f1, then mk f1 ≤ mk f2.

Русский

Если существует g: A1 → A2 и g ≫ f2 = f1, то mk f1 ≤ mk f2.

LaTeX

$$$mk f_1 \\le mk f_2$ when $(g: A_1 \\to A_2)$ and $(w: g \\;\\; f_2 = f_1)$$$

Lean4

theorem mk_le_of_comm {B A : C} {X : Subobject B} {f : A ⟶ B} [Mono f] (g : A ⟶ (X : C)) (w : g ≫ X.arrow = f) :
    mk f ≤ X :=
  le_of_comm ((underlyingIso f).hom ≫ g) <| by simp [w]

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

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

Разделы

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

Аффилиация

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