hasAffineProperty — Mathlib

English

There is an affine property for the class IsSeparated: it defines HasAffineProperty.

Русский

У класса IsSeparated есть аффинное свойство: задаётся HasAffineProperty.

LaTeX

$$HasAffineProperty @IsSeparated$$

Lean4

instance hasAffineProperty : HasAffineProperty @IsSeparated fun X _ _ _ ↦ X.IsSeparated :=
  by
  convert HasAffineProperty.of_isZariskiLocalAtTarget @IsSeparated with X Y f hY
  rw [Scheme.isSeparated_iff, ← terminal.comp_from f, IsSeparated.comp_iff]
  rfl

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