English
Let X and Y be topological spaces and f: X → Y an embedding. A subset s of X is locally closed if and only if there exists a locally closed subset s' of Y such that s' ∩ range(f) = f''s (the image of s under f).
Русский
Пусть X и Y — топологические пространства, f: X → Y — вложение. множество s ⊆ X локально замкнуто тогда и только тогда существует локально замкнутое множество s' ⊆ Y такое, что s' ∩ range(f) = f''s (образ s под f).
LaTeX
$$$ \mathrm{IsLocallyClosed}(s) \iff \exists s' \subseteq Y, \ \mathrm{IsLocallyClosed}(s') \land s' \cap \mathrm{range}(f) = f'' s$$$
Lean4
theorem isLocallyClosed_iff {s : Set X} {f : X → Y} (hf : IsEmbedding f) :
IsLocallyClosed s ↔ ∃ s' : Set Y, IsLocallyClosed s' ∧ s' ∩ range f = f '' s := by
simp_rw [hf.isInducing.isLocallyClosed_iff, ← (image_injective.mpr hf.injective).eq_iff,
image_preimage_eq_inter_range]
