inf

Mathlib.CategoryTheory.MorphismProperty.Basic

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

← MathLib Explorer

English

If P has RespectsIso, then P.op has RespectsIso.

Русский

Если P имеет свойство RespectsIso, то P.op имеет это свойство.

LaTeX

$$$[P\RespectsIso] \Rightarrow [P^{op}.\mathrm{RespectsIso}]$$$

Lean4

instance inf (P₁ P₂ Q : MorphismProperty C) [P₁.RespectsRight Q] [P₂.RespectsRight Q] : (P₁ ⊓ P₂).RespectsRight Q where
  postcomp i hi f hf := ⟨postcomp i hi f hf.left, postcomp i hi f hf.right⟩

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

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

Разделы

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

Аффилиация

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