continuous

Mathlib.AlgebraicGeometry.Scheme

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

English

If a point x in a scheme X is closed, then its height is zero.

Русский

Если точка x в схеме X является замкнутой, то её высота равна нулю.

LaTeX

$$$\text{IsClosed}\{x\} \Rightarrow \operatorname{height}(x) = 0$$$

Lean4

@[continuity, fun_prop]
theorem continuous {X Y : Scheme} (f : X.Hom Y) : Continuous f.base :=
  f.base.hom.2

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

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

Разделы

Аффилиация

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