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]