English
If f is an inducing map, then s is σ-compact if and only if its image f[s] is σ-compact.
Русский
Если f — индуктивное отображение, то s σ-компактно тогда и только тогда, когда образ f[s] σ-компактен.
LaTeX
$$$IsInducing f \\rightarrow (IsSigmaCompact s \\leftrightarrow IsSigmaCompact (f''s))$$$
Lean4
/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is σ-compact
if and only `s` is σ-compact. -/
theorem isSigmaCompact_iff {f : X → Y} {s : Set X} (hf : IsInducing f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s) :=
by
constructor
· exact fun h ↦ h.image hf.continuous
· rintro
⟨L, hcomp, hcov⟩
-- Suppose f(s) is σ-compact; we want to show s is σ-compact.
-- Write f(s) as a union of compact sets L n, so s = ⋃ K n with K n := f⁻¹(L n) ∩ s.
-- Since f is inducing, each K n is compact iff L n is.
refine ⟨fun n ↦ f ⁻¹' (L n) ∩ s, ?_, ?_⟩
· intro n
have : f '' (f ⁻¹' (L n) ∩ s) = L n :=
by
rw [image_preimage_inter, inter_eq_left.mpr]
exact (subset_iUnion _ n).trans hcov.le
apply hf.isCompact_iff.mpr (this.symm ▸ (hcomp n))
·
calc
⋃ n, f ⁻¹' L n ∩ s
_ = f ⁻¹' (⋃ n, L n) ∩ s := by rw [preimage_iUnion, iUnion_inter]
_ = f ⁻¹' (f '' s) ∩ s := by rw [hcov]
_ = s := inter_eq_right.mpr (subset_preimage_image _ _)
