overPost — Mathlib

English

For any C, D, J and F with PreservesLimitsOfShape (WithTerminal J) F, the shape-preserving property transfers to Over.post F for shape J.

Русский

Для любых C, D, J и F с PreservesLimitsOfShape (WithTerminal J) F свойство сохранения формы переходит к Over.post F для формы J.

LaTeX

$$$\text{PreservesLimitsOfShape } J (\mathrm{Over.post}\ F)$$$

Lean4

instance overPost [PreservesLimitsOfShape (WithTerminal J) F] : PreservesLimitsOfShape J (Over.post F (X := X)) where
  preservesLimit.preserves {coneK}
    isLimitConeK :=
    have isLimitConeD :=
      (IsLimit.postcomposeHomEquiv liftFromOverComp.symm _).symm <|
        isLimitOfPreserves F (isLimitEquiv.symm isLimitConeK)
    ⟨isLimitEquiv <|
        isLimitConeD.ofIsoLimit <|
          Cones.ext (.refl _) fun
            | .star | .of a => by aesop⟩

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