ofRetract — Mathlib

English

If Y is a retract of X and X is internally projective, then Y is internally projective.

Русский

Если Y является retract'ом X, и X внутри проективен, то Y тоже проективен.

LaTeX

$$$ (\\text{Retract } Y X) \\Rightarrow (\\mathrm{InternallyProjective}(X) \\Rightarrow \\mathrm{InternallyProjective}(Y)). $$$

Lean4

theorem ofRetract {X Y : C} (r : Retract Y X) [InternallyProjective X] : InternallyProjective Y :=
  ⟨isInternallyProjective.prop_of_retract r (isInternallyProjective.prop_of_is _)⟩

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