instIsStableUnderRetractsMin — Mathlib

English

The minimum (greatest lower bound) of retract-stable properties is retract-stable.

Русский

Наименьшее (наибольшая нижняя граница) свойств, стабильных на retracts, сохраняет retracts.

LaTeX

$$(min(P1,P2)).IsStableUnderRetracts$$

Lean4

instance (P₁ P₂ : MorphismProperty C) [P₁.IsStableUnderRetracts] [P₂.IsStableUnderRetracts] :
    (P₁ ⊓ P₂).IsStableUnderRetracts where of_retract := fun h ⟨h₁, h₂⟩ ↦ ⟨of_retract h h₁, of_retract h h₂⟩

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