toOpens

Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens

Lean4

/-- The inclusion from `X.AffineZariskiSite` to `X.Opens`. -/
abbrev toOpens (U : X.AffineZariskiSite) : X.Opens :=
  U.1

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

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

Разделы

Аффилиация

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