iSup_opensRange — Mathlib

English

The supremum over i of the opensRange of 𝒰.f i is the top element.

Русский

Наивысшая верхняя граница (супремум) по i от opensRange 𝒰.f i равна верхнему элементу.

LaTeX

$$$$ \big\lceil i \big\rceil \operatorname{opensRange}(\mathcal{U}.f i) = \top $$$$

Lean4

theorem iSup_opensRange {X : Scheme.{u}} (𝒰 : X.OpenCover) : ⨆ i, (𝒰.f i).opensRange = ⊤ :=
  Opens.ext <| by rw [Opens.coe_iSup]; exact 𝒰.iUnion_range

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