instIsSmoothOfRelativeDimensionOfNatNatOfIsOpenImmersion

English

Open immersions are smooth of relative dimension 0.

Русский

Открытые вложения гладки относительно размерности 0.

LaTeX

$$IsSmoothOfRelativeDimension(0) f for open immersion f$$

Lean4

/-- Open immersions are smooth of relative dimension `0`. -/
instance (priority := 900) [IsOpenImmersion f] : IsSmoothOfRelativeDimension 0 f :=
  HasRingHomProperty.of_isOpenImmersion
    (locally_holdsForLocalizationAway <|
        isStandardSmoothOfRelativeDimension_holdsForLocalizationAway).containsIdentities

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