universally_le

Mathlib.CategoryTheory.MorphismProperty.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.universally_le

← MathLib Explorer

English

The universally extended P is contained in P: P.universally ≤ P.

Русский

Универсальное расширение P содержится в P: P.universally ≤ P.

LaTeX

$$$P^{\mathrm{universally}} \le P$$$

Lean4

theorem universally_le (P : MorphismProperty C) : P.universally ≤ P :=
  by
  intro X Y f hf
  exact hf (𝟙 _) (𝟙 _) _ (IsPullback.of_vert_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩)

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

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

Разделы

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

Аффилиация

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