affineOpensRestrict_symm_apply_coe

English

The symmetry of the affineOpensRestrict equivalence sends V to the underlying open subset U with coefficient given by U.ι.

Русский

Обратная операция эквивалентности affineOpensRestrict отправляет V в связанное открытое подмножество U с коэффициентом, заданным U.ι.

LaTeX

$$((affineOpensRestrict U).symm V).1 = U.ι ⁻¹ᵁ V$$

Lean4

@[simp]
theorem _root_.AlgebraicGeometry.affineOpensRestrict_symm_apply_coe {X : Scheme.{u}} (U : X.Opens) (V) :
    ((affineOpensRestrict U).symm V).1 = U.ι ⁻¹ᵁ V :=
  rfl

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