of_openCover — Mathlib

English

If iSup of opens equals top, then P(f) is equivalent to P on each restricted part.

Русский

Если iSup открытых множеств равен вершине, то P(f) эквивалентно P на каждой части, ограниченной.

LaTeX

$$$P(f) \\iff \\forall i, P(f|_{U_i})$$$

Lean4

theorem of_openCover (H : ∀ i, P (𝒰.pullbackHom f i)) : P f :=
  by
  apply of_iSup_eq_top (fun i ↦ (𝒰.f i).opensRange) 𝒰.iSup_opensRange
  exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (H i)

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