iSup_affineOpens_eq_top — Mathlib

English

The supremum of all affine opens equals the top open set.

Русский

Образующий сверху объединение всех аффинных открытых равняется верхнему открытию.

LaTeX

$$$$ i\!\!\sup_{i: X.\text{affineOpens}} (i:\ X.\text{Opens}) = \top. $$$$

Lean4

theorem iSup_affineOpens_eq_top (X : Scheme) : ⨆ i : X.affineOpens, (i : X.Opens) = ⊤ :=
  by
  apply Opens.ext
  rw [Opens.coe_iSup]
  apply IsTopologicalBasis.sUnion_eq
  rw [← Set.image_eq_range]
  exact isBasis_affine_open X

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