basicOpen_of_isUnit

Mathlib.AlgebraicGeometry.Scheme

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

English

If f is a unit, then X.basicOpen f equals U.

Русский

Если f является единицей, то X.basicOpen f равняется U.

LaTeX

$$$\\text{If } f \\text{ is a unit } X.basicOpen f = U$$$

Lean4

theorem basicOpen_of_isUnit {f : Γ(X, U)} (hf : IsUnit f) : X.basicOpen f = U :=
  RingedSpace.basicOpen_of_isUnit _ hf

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

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

Разделы

Аффилиация

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