isLocallyClosed_iff_coe_preimage — Mathlib

English

An open cover preserves local closedness: s is locally closed iff all restricted preimages are locally closed.

Русский

Открытое покрытие сохраняет локальную замкнутость: s локально замкнуто тогда и только тогда, когда все ограниченные прообраза локально замкнуты.

LaTeX

$$$IsLocallyClosed s \\iff \\forall i, IsLocallyClosed ((↑)^{-1}' s : Set (U i))$$$

Lean4

theorem isLocallyClosed_iff_coe_preimage {s : Set β} :
    IsLocallyClosed s ↔ ∀ i, IsLocallyClosed ((↑) ⁻¹' s : Set (U i)) :=
  by
  have (i : _) : coborder ((↑) ⁻¹' s : Set (U i)) = Subtype.val ⁻¹' coborder s :=
    (U i).isOpen.isOpenEmbedding_subtypeVal.coborder_preimage _
  simp [isLocallyClosed_iff_isOpen_coborder, hU.isOpen_iff_coe_preimage, this]

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