toScheme_carrier

Mathlib.AlgebraicGeometry.Restrict

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

English

The carrier of U (as a scheme) equals the carrier of U viewed as a subset of X.

Русский

Множество точек U как схемы совпадает с тем же множеством точек, рассмотренным как подмножество X.

LaTeX

$$U.toScheme.carrier.carrier = (U : Set X).Elem$$

Lean4

theorem toScheme_carrier : (U : Type u) = (U : Set X) :=
  rfl

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

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

Разделы

Аффилиация

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