basicOpen_le

Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

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

English

The basicOpen construction is monotone with respect to inclusions.

Русский

Конструкция basicOpen монотонна по включениям.

LaTeX

$$$U.basicOpen f \\le U$$$

Lean4

theorem basicOpen_le (U : X.AffineZariskiSite) (f : Γ(X, U.toOpens)) : U.basicOpen f ≤ U :=
  ⟨f, rfl⟩

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

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

Разделы

Аффилиация

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