English
If f is an IsUniformInducing map, then IsComplete (f''s) iff IsComplete s holds for the image.
Русский
Если f — равномерно-индуцирующее отображение, тогда IsComplete(образ) эквивалентно IsComplete исходного множества.
LaTeX
$$$\\text{IsUniformInducing}(f) \\Rightarrow (\\text{IsComplete}(f''s) \\Leftrightarrow \\text{IsComplete}(s))$$$
Lean4
/-- A set is complete iff its image under a uniform inducing map is complete. -/
theorem isComplete_image_iff {m : α → β} {s : Set α} (hm : IsUniformInducing m) : IsComplete (m '' s) ↔ IsComplete s :=
by
have fact1 : SurjOn (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := surjOn_image .. |>.filter_map_Iic
have fact2 : MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := mapsTo_image .. |>.filter_map_Iic
simp_rw [IsComplete, imp.swap (a := Cauchy _), ← mem_Iic (b := 𝓟 _), fact1.forall fact2, hm.cauchy_map_iff,
exists_mem_image, map_le_iff_le_comap, hm.isInducing.nhds_eq_comap]
