English
If f is continuous and injective, then f(derivedSet A) ⊆ derivedSet(f(A)).
Русский
Если f непрерывна и инъективна, то изображение производного множества под действием f содержится в производном множестве образа: f(derivedSet A) ⊆ derivedSet(f(A)).
LaTeX
$$$$\operatorname{image}(f, \operatorname{derivedSet}(A)) \subseteq \operatorname{derivedSet}(\operatorname{image}(f, A)).$$$$
Lean4
theorem image_derivedSet {β : Type*} [TopologicalSpace β] {A : Set X} {f : X → β} (hf1 : Continuous f)
(hf2 : Function.Injective f) : f '' derivedSet A ⊆ derivedSet (f '' A) :=
by
intro x hx
simp only [Set.mem_image, mem_derivedSet] at hx
obtain ⟨y, hy1, rfl⟩ := hx
convert hy1.map hf1.continuousAt hf2
simp
