image_of_continuousOn — Mathlib

English

Let s be a σ-compact subset of X and f be continuous on s. Then the image f[s] is σ-compact.

Русский

Пусть s — σ-компактное подмножество X, и f непрерывна на s. Тогда образ f[s] является σ-компактным.

LaTeX

$$$IsSigmaCompact(s) \\\\rightarrow ContinuousOn(f,s) \\\\rightarrow IsSigmaCompact(f''s)$$$

Lean4

/-- If `s` is σ-compact and `f` is continuous on `s`, `f(s)` is σ-compact. -/
theorem image_of_continuousOn {f : X → Y} {s : Set X} (hs : IsSigmaCompact s) (hf : ContinuousOn f s) :
    IsSigmaCompact (f '' s) := by
  rcases hs with ⟨K, hcompact, hcov⟩
  refine ⟨fun n ↦ f '' K n, ?_, hcov.symm ▸ image_iUnion.symm⟩
  exact fun n ↦ (hcompact n).image_of_continuousOn (hf.mono (hcov.symm ▸ subset_iUnion K n))

Похожие утверждения