preimage_of_isIso — Mathlib

English

If U ⊆ Y is affine open and f: X ⟶ Y is an isomorphism, then the preimage f^{-1}(U) is affine open in X.

Русский

Если U ⊆ Y аффинное открытое и f: X ⟶ Y является изоморфизмом, то прообраз f^{-1}(U) является аффинным открытым в X.

LaTeX

$$IsAffineOpen (f ⁻¹ᵁ U)$$

Lean4

theorem preimage_of_isIso {U : Y.Opens} (hU : IsAffineOpen U) (f : X ⟶ Y) [IsIso f] : IsAffineOpen (f ⁻¹ᵁ U) :=
  haveI : IsAffine _ := hU
  .of_isIso (f ∣_ U)

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