instIsClosedUnderIsomorphismsShift

English

If P is closed under isomorphisms, then for any a, the shifted property P.shift a is also closed under isomorphisms.

Русский

Если P сохраняет изоморфизмов, то и свойство P.shift a также сохраняет изоморфизмы.

LaTeX

$$$P.IsClosedUnderIsomorphisms \Rightarrow (P.shift a).IsClosedUnderIsomorphisms$$$

Lean4

instance (a : A) [P.IsClosedUnderIsomorphisms] : (P.shift a).IsClosedUnderIsomorphisms where
  of_iso e hX := P.prop_of_iso ((shiftFunctor C a).mapIso e) hX

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