of_iSup_eq_top — Mathlib

English

If P holds on all pullbacks along an open cover, then P(f) holds.

Русский

Если P выполняется на всех обратных ограничениях вдоль открытого покрытия, то P(f) действительно выполняется.

LaTeX

$$$\\forall i, P( pullback(f, i) ) \\Rightarrow P(f)$$$

Lean4

theorem of_iSup_eq_top {ι} (U : ι → Y.Opens) (hU : iSup U = ⊤) (H : ∀ i, P (f ∣_ U i)) : P f :=
  by
  refine
    (P.iff_of_zeroHypercover_target (Y.openCoverOfIsOpenCover (s := Set.range U) Subtype.val (by ext; simp [← hU]))).mpr
      fun i ↦ ?_
  obtain ⟨_, i, rfl⟩ := i
  refine (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mp ?_
  change P (f ∣_ (U i).ι.opensRange)
  rw [Scheme.Opens.opensRange_ι]
  exact H i

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