component_nontrivial — Mathlib

English

If X is integral, then its underlying topological space is irreducible.

Русский

Если схема X целостна, то её связанное топологическое пространство неприводимо.

LaTeX

$$$\text{IsIntegral}(X) \Rightarrow \operatorname{IrreducibleSpace}(|X|)$$$

Lean4

instance component_nontrivial (X : Scheme.{u}) (U : X.Opens) [Nonempty U] : Nontrivial Γ(X, U) :=
  LocallyRingedSpace.component_nontrivial (hU := ‹_›)

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