image_of_isOpenImmersion — Mathlib

English

If f: X ⟶ Y is an open immersion and U ⊆ X is affine open, then the image f''ᵁ U is an affine open in Y.

Русский

Если f: X ⟶ Y является открытым вложением и U ⊆ X аффинное открытое, то образ f''ᵁ U является аффинным открытым в Y.

LaTeX

$$IsAffineOpen (f ''ᵁ U)$$

Lean4

theorem image_of_isOpenImmersion (f : X ⟶ Y) [H : IsOpenImmersion f] : IsAffineOpen (f ''ᵁ U) :=
  by
  have : IsAffine _ := hU
  convert isAffineOpen_opensRange (U.ι ≫ f)
  ext1
  exact Set.image_eq_range _ _

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