isDominant_ι — Mathlib

English

Let X be a scheme and U an open dense subset of X. The inclusion morphism ι: U → X is dominant.

Русский

Пусть X — схема, U — открытое плотное подмножество X. Включение ι: U → X является доминирующим отображением.

LaTeX

$$$\mathrm{IsDominant}(U \hookrightarrow X)$$$

Lean4

theorem isDominant_ι {U : X.Opens} (hU : Dense (X := X) U) : IsDominant U.ι :=
  ⟨by simpa [DenseRange] using hU⟩

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