retracts_monotone — Mathlib

English

Let P and Q be morphism properties on a category with P ⊆ Q. Then retracts(P) ⊆ retracts(Q). In words, the operation of taking retracts is monotone with respect to inclusion of properties.

Русский

Пусть P и Q — свойства морфизмов в категории, причём P ⊆ Q. Тогда retracts(P) ⊆ retracts(Q). Иными словами, операция взятия retracts монотонна по включению свойств.

LaTeX

$$$\forall {\mathcal C} \ (P \le Q) \,\Rightarrow \, \operatorname{retracts}(P) \le \operatorname{retracts}(Q) $$$

Lean4

theorem retracts_monotone : Monotone (retracts (C := C)) :=
  by
  intro _ _ h _ _ _ ⟨_, _, _, hg, hg'⟩
  exact ⟨_, _, _, hg, h _ hg'⟩

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