iff_of_isOpenCover — Mathlib

English

For an open cover U, locally constructible s is equivalent to the property that each s ∩ U_i is locally constructible.

Русский

Для открытого покрытия U локальная конструируемость s эквивалентна тому, что каждый s ∩ U_i локально конструируем.

LaTeX

$$$\\operatorname{IsLocallyConstructible}(s) \\iff \\forall i, \\operatorname{IsLocallyConstructible}(s \\cap (U_i : Set X)).$$$

Lean4

theorem iff_of_isOpenCover (hU : IsOpenCover U) :
    IsLocallyConstructible s ↔ ∀ i, IsLocallyConstructible ((U i : Set X) ↓∩ s) :=
  ⟨fun H i ↦ H.preimage_of_isOpenEmbedding (U i).2.isOpenEmbedding_subtypeVal, fun H ↦ .of_isOpenCover hU H⟩

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