isAffineOpen_bot

Mathlib.AlgebraicGeometry.Limits

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.isAffineOpen_bot

English

The bottom open subset of a scheme X is affine open.

Русский

Нижняя открытая подмножество схемы X аффинно открытое.

LaTeX

$$$\\text{IsAffineOpen}(\\bot : X.OPEN)$$$

Lean4

theorem isAffineOpen_bot (X : Scheme) : IsAffineOpen (⊥ : X.Opens) :=
  @isAffine_of_isEmpty _ (inferInstanceAs (IsEmpty (∅ : Set X)))

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru