isCompactOpen_iff_eq_finset_affine_union

English

An open subset is compact if and only if it can be expressed as a finite union of basic affine opens.

Русский

Открытая подмножество компактно тогда, когда его можно выразить как конечное объединение базовых аффинных открытых подмножеств.

LaTeX

$$$\text{IsCompact}(U) \land \text{IsOpen}(U) \iff \exists S, S.finite \land U = \bigcup_{i\in S} (\text{basic open subset})$$$

Lean4

theorem isCompactOpen_iff_eq_finset_affine_union {X : Scheme} (U : Set X) :
    IsCompact U ∧ IsOpen U ↔ ∃ s : Set X.affineOpens, s.Finite ∧ U = ⋃ i ∈ s, i :=
  by
  apply Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion (fun (U : X.affineOpens) => (U : X.Opens))
  · rw [Subtype.range_coe]; exact isBasis_affine_open X
  · exact fun i => i.2.isCompact

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