isOpenCover_opensRange — Mathlib

English

The iSup of the opensRange over an open cover equals the top element.

Русский

iSup от opensRange по открытому покрытию равен верхнему элементу.

LaTeX

$$$$ \mathrm{iSup}\;\operatorname{opensRange}(\mathcal{U}.f i) = \top $$$$

Lean4

/-- The ranges of the maps in a scheme-theoretic open cover are a topological open cover. -/
theorem isOpenCover_opensRange {X : Scheme.{u}} (𝒰 : X.OpenCover) : IsOpenCover fun i ↦ (𝒰.f i).opensRange :=
  .mk 𝒰.iSup_opensRange

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