isAffineOpen_top

Mathlib.AlgebraicGeometry.AffineScheme

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

← MathLib Explorer

English

Gamma is an equivalence (IsEquivalence).

Русский

Γ является эквивалентностью (IsEquivalence).

LaTeX

$$$$ \text{Γ is an equivalence}. $$$$

Lean4

theorem isAffineOpen_top (X : Scheme) [IsAffine X] : IsAffineOpen (⊤ : X.Opens) :=
  by
  convert isAffineOpen_opensRange (𝟙 X)
  ext1
  exact Set.range_id.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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