opensRange_fromSpec

Mathlib.AlgebraicGeometry.AffineScheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec

English

The openness range of the fromSpec map is exactly U; i.e., the open range equals U.

Русский

Область открытости из fromSpec ровно U; то есть открытый диапазон равен U.

LaTeX

$$hU.fromSpec.opensRange = U$$

Lean4

@[simp]
theorem opensRange_fromSpec : hU.fromSpec.opensRange = U :=
  Opens.ext (range_fromSpec hU)

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

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

Разделы

Аффилиация

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