isOpen_preimage_val_closure — Mathlib

English

If s is locally closed, then closure(s) ∩ s is open in the ambient space, i.e., open in the closure of s.

Русский

Если s локально замкнуто, то closure(s) ∩ s открыто в пространстве, то есть открыто внутри closure(s).

LaTeX

$$$ \mathrm{IsLocallyClosed}(s) \Rightarrow \mathrm{IsOpen}(\mathrm{closure}(s) \downarrow \cap s)$$$

Lean4

theorem isOpen_preimage_val_closure (hs : IsLocallyClosed s) : IsOpen (closure s ↓∩ s) :=
  ((isLocallyClosed_tfae s).out 0 4).mp hs

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