of_iSup_eq_top — Mathlib

English

If a family of opens U: ι → X covers X in the sense that iSup U = ⊤, and P((U i).ι ≫ f) holds for every i, then P f holds.

Русский

Если семейство открытых подмножеств U: ι → X покрывает X (iSup U = ⊤) и для каждого i выполняется P((U i).ι ≫ f), то P f выполняется.

LaTeX

$$$\forall ι (U : ι \to X^{\mathrm{Opens}}), \; (iSup U = \top) \; \Rightarrow \Big( \forall i, P((U i).\iota \gg f) \Big) \Rightarrow P f.$$$

Lean4

theorem of_iSup_eq_top {ι} (U : ι → X.Opens) (hU : iSup U = ⊤) (H : ∀ i, P ((U i).ι ≫ f)) : P f :=
  by
  refine
    (P.iff_of_zeroHypercover_source (X.openCoverOfIsOpenCover (s := Set.range U) Subtype.val (by ext; simp [← hU]))).mpr
      fun i ↦ ?_
  obtain ⟨_, i, rfl⟩ := i
  exact H i

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