isOpenImmersion_isStableUnderComposition

English

IsOpenImmersion respects isomorphisms: if f is an open immersion, so is any isomorphic copy.

Русский

IsOpenImmersion сохраняет изоморфизмы: если f — открытое вложение, то и его изоморфная копия.

LaTeX

$$$ \text{isOpenImmersion}_\text{respectsIso}$$$

Lean4

instance isOpenImmersion_isStableUnderComposition : MorphismProperty.IsStableUnderComposition @IsOpenImmersion where
  comp_mem f g _ _ := LocallyRingedSpace.IsOpenImmersion.comp f.toLRSHom g.toLRSHom

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