le_retractClosure — Mathlib

English

Let P be a property of objects in a category C. If X satisfies P, then X lies in the retract-closure of P, i.e. X is a retract of itself (via the identity) from a P-object. Therefore P ≤ retractClosure P.

Русский

Пусть P — свойство объектов в категории C. Если X удовлетворяет P, то X принадлежит замыканию по ретракциям P, то есть X является ретрактом самого себя (с помощью тождественного мономорфизма) из объекта, удовлетворяющего P. Следовательно, P ≤ retractClosure P.

LaTeX

$$$P \le \operatorname{retractClosure}(P)$$$

Lean4

theorem le_retractClosure : P ≤ retractClosure P := fun X hX => ⟨X, hX, ⟨Retract.refl X⟩⟩

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