ofLEMk

Mathlib.CategoryTheory.Subobject.Basic

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

← MathLib Explorer

English

The composition of X.ofLEMk f h with f equals X.arrow.

Русский

Составление X.ofLEMk f h с f равно X.arrow.

LaTeX

$$$(X.ofLEMk f h) \\;\\gg f = X.arrow$$$

Lean4

/-- An inequality of subobjects is witnessed by some morphism between the corresponding objects. -/
def ofLEMk {B A : C} (X : Subobject B) (f : A ⟶ B) [Mono f] (h : X ≤ mk f) : (X : C) ⟶ A :=
  ofLE X (mk f) h ≫ (underlyingIso f).hom

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

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

Разделы

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

Аффилиация

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