monotone_isoClosure

Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.monotone_isoClosure

English

If P is contained in Q, then the iso-closure of P is contained in the iso-closure of Q.

Русский

Если P ⊆ Q, то isoClosure(P) ⊆ isoClosure(Q).

LaTeX

$$$$ P \le Q \Rightarrow isoClosure(P) \le isoClosure(Q). $$$$

Lean4

theorem monotone_isoClosure (h : P ≤ Q) : isoClosure P ≤ isoClosure Q :=
  by
  rintro X ⟨X', hX', ⟨e⟩⟩
  exact ⟨X', h _ hX', ⟨e⟩⟩

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

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

Разделы

Аффилиация

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