English
The image of a compact set under a continuous map on it is compact.
Русский
Образ компактного множества при ограничении непрерывной функцией на нем компактён.
LaTeX
$$$IsCompact(s) \rightarrow ContinuousOn(f, s) \rightarrow IsCompact(f''s)$$$
Lean4
theorem image_of_continuousOn {f : X → Y} (hs : IsCompact s) (hf : ContinuousOn f s) : IsCompact (f '' s) :=
by
intro l lne ls
have : NeBot (l.comap f ⊓ 𝓟 s) := comap_inf_principal_neBot_of_image_mem lne (le_principal_iff.1 ls)
obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, ClusterPt x (l.comap f ⊓ 𝓟 s) := @hs _ this inf_le_right
haveI := hx.neBot
use f x, mem_image_of_mem f hxs
have : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l) :=
by
convert (hf x hxs).inf (@tendsto_comap _ _ f l) using 1
rw [nhdsWithin]
ac_rfl
exact this.neBot
