finiteSubcover — Mathlib

Lean4
/-- Every open cover of a quasi-compact scheme can be refined into a finite subcover.
-/
@[simps! X f]
def finiteSubcover {X : Scheme.{u}} (𝒰 : OpenCover X) [H : CompactSpace X] : OpenCover X :=
  by
  have :=
    @CompactSpace.elim_nhds_subcover _ _ H (fun x : X => Set.range (𝒰.f (𝒰.idx x)).base) fun x =>
      (IsOpenImmersion.isOpen_range (𝒰.f (𝒰.idx x))).mem_nhds (𝒰.covers x)
  let t := this.choose
  have h : ∀ x : X, ∃ y : t, x ∈ Set.range (𝒰.f (𝒰.idx y)).base :=
    by
    intro x
    have h' : x ∈ (⊤ : Set X) := trivial
    rw [← Classical.choose_spec this, Set.mem_iUnion] at h'
    rcases h' with ⟨y, _, ⟨hy, rfl⟩, hy'⟩
    exact ⟨⟨y, hy⟩, hy'⟩
  exact
    { I₀ := t
      X := fun x => 𝒰.X (𝒰.idx x.1)
      f := fun x => 𝒰.f (𝒰.idx x.1)
      mem₀ := by
        rw [presieve₀_mem_precoverage_iff]
        exact ⟨h, inferInstance⟩ }
Похожие утверждения