mk

Mathlib.CategoryTheory.MorphismProperty.Comma

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

Lean4

/-- Make an object of `P.Over Q X` from a morphism `f : A ⟶ X` and a proof of `P f`. -/
@[simps hom left]
protected def mk {A : T} (f : A ⟶ X) (hf : P f) : P.Over Q X
    where
  left := A
  right := ⟨⟨⟩⟩
  hom := f
  prop := hf

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

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

Разделы

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

Аффилиация

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