iff_isConstructible_of_isOpenCover

English

For an open cover U with compact pieces, locally constructible s is equivalent to each s ∩ U_i being constructible.

Русский

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

LaTeX

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

Lean4

theorem iff_isConstructible_of_isOpenCover [PrespectralSpace X] [QuasiSeparatedSpace X] (hU : IsOpenCover U)
    (hU' : ∀ i, IsCompact (U i : Set X)) : IsLocallyConstructible s ↔ ∀ i, IsConstructible (s ∩ U i) :=
  ⟨fun H i ↦ H.inter_of_isOpen_isCompact (U i).2 (hU' i), fun H ↦
    .of_isOpenCover' hU fun i ↦ (H i).isLocallyConstructible⟩

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