isCompact_iff — Mathlib

English

If f is an embedding, then a set s is compact iff its image under f is compact.

Русский

Если f — вложение, тогда множество s компактно тогда и только тогда, когда образ f(s) компактен.

LaTeX

$$IsCompact(s) ⇔ IsCompact(f''s)$$

Lean4

/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is compact
  if and only if `s` is compact. -/
theorem isCompact_iff {f : X → Y} (hf : IsInducing f) : IsCompact s ↔ IsCompact (f '' s) :=
  by
  refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot F_le => ?_⟩
  obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ := hs ((map_mono F_le).trans_eq map_principal)
  exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

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