English
Let s ⊆ X be locally closed in a space X. If f: X → Y is inducing (IsInducing f) and range f is locally closed in Y, then the image f''s is locally closed in Y.
Русский
Пусть s ⊆ X локально замкнуто в X. Тогда при отображении f: X → Y, являющемся индуцирующим, и если образ range(f) локально замкнут в Y, то образ f''s локально замкнут в Y.
LaTeX
$$$ \\mathrm{IsLocallyClosed}(s) \\land \\mathrm{IsInducing}(f) \\land \\mathrm{IsLocallyClosed}(\\mathrm{range}(f)) \\;\Rightarrow\\; \\mathrm{IsLocallyClosed}(f'' s)$$$
Lean4
theorem image {s : Set X} (hs : IsLocallyClosed s) {f : X → Y} (hf : IsInducing f) (hf' : IsLocallyClosed (range f)) :
IsLocallyClosed (f '' s) := by
obtain ⟨t, ht, rfl⟩ := hf.isLocallyClosed_iff.mp hs
rw [image_preimage_eq_inter_range]
exact ht.inter hf'
