openCoverOfIsOpenCover — Mathlib

English

If a family of open sets U i covers X, the restricted data X.restrict U forms an open cover of X.

Русский

Если семейство открытых подмножеств U i покрывает X, то ограничение X.restrict U образует открытое покрытие X.

LaTeX

$$$ X.OpenCover $$$

Lean4

/-- If `U` is a family of open sets that covers `X`, then `X.restrict U` forms an `X.open_cover`. -/
@[simps! I₀ X f]
def openCoverOfIsOpenCover {s : Type*} (X : Scheme.{u}) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) :
    X.OpenCover where
  I₀ := s
  X i := U i
  f i := (U i).ι
  mem₀ := by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, inferInstance⟩
    have hx : x ∈ ⨆ i, U i := hU.symm ▸ show x ∈ (⊤ : X.Opens) by trivial
    rw [Opens.mem_iSup] at hx
    obtain ⟨i, hi⟩ := hx
    use i
    simpa

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