isCompactOpen_iff_eq_basicOpen_union

English

Under an affine scheme, a compact open subset can be expressed as a finite union of basic opens.

Русский

Для аффинной схемы компактное открытое множество раскладывается в конечное объединение базовых открытых множеств.

LaTeX

$$$\text{IsCompact}(U) \land \text{IsOpen}(U) \Rightarrow \exists s : \text{Set}(\Gamma(X, \top)), s.finite \land U = \bigcup_{i\in s} X.basicOpen(i)$$$

Lean4

theorem isCompactOpen_iff_eq_basicOpen_union {X : Scheme} [IsAffine X] (U : Set X) :
    IsCompact U ∧ IsOpen U ↔ ∃ s : Set Γ(X, ⊤), s.Finite ∧ U = ⋃ i ∈ s, X.basicOpen i :=
  (isBasis_basicOpen X).isCompact_open_iff_eq_finite_iUnion _ (fun _ => ((isAffineOpen_top _).basicOpen _).isCompact) _

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