instIsIntegralToSchemeOfNonemptyCarrierCarrierCommRingCat

Mathlib.AlgebraicGeometry.FunctionField

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instIsIntegralToSchemeOfNonemptyCarrierCarrierCommRingCat

English

If X is integral and U is a nonempty open subset, then U is integral.

Русский

Если X целый, то любой непустой открытый подмножество U также целое.

LaTeX

$$$[\operatorname{IsIntegral}(X)],\ \text{Nonempty }U\Rightarrow \operatorname{IsIntegral}(U).$$$

Lean4

instance {X : Scheme} [IsIntegral X] {U : X.Opens} [Nonempty U] : IsIntegral U :=
  isIntegral_of_isOpenImmersion U.ι

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

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

Разделы

Аффилиация

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