instIsStableUnderShiftByIsoClosure

English

For a given a, if P is stable under shift by a, then P.isoClosure.IsStableUnderShiftBy a.

Русский

Для данного a, если P стабильно относительно сдвига на a, то P.isoClosureIsStableUnderShiftBy a.

LaTeX

$$$\forall a,\ (P.IsStableUnderShiftBy a) \Rightarrow P.isoClosure.IsStableUnderShiftBy a$$$

Lean4

instance (a : A) [P.IsStableUnderShiftBy a] : P.isoClosure.IsStableUnderShiftBy a where
  le_shift := by
    rintro X ⟨Y, hY, ⟨e⟩⟩
    exact ⟨Y⟦a⟧, P.le_shift a _ hY, ⟨(shiftFunctor C a).mapIso e⟩⟩

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