ofMkLEMk_comp

Mathlib.CategoryTheory.Subobject.Basic

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

← MathLib Explorer

English

The constructed morphism ofMkLEMk satisfies the equation with g: ofMkLEMk f g h ≫ g = f.

Русский

Собранный мороморфизм ofMkLEMk удовлетворяет равенству: ofMkLEMk f g h ≫ g = f.

LaTeX

$$$\operatorname{ofMkLEMk} f g h \;\ggong g = f$$$

Lean4

@[simp]
theorem ofMkLEMk_comp {B A₁ A₂ : C} {f : A₁ ⟶ B} {g : A₂ ⟶ B} [Mono f] [Mono g] (h : mk f ≤ mk g) :
    ofMkLEMk f g h ≫ g = f := by simp [ofMkLEMk]

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

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

Разделы

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

Аффилиация

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