isLindelof_iff — Mathlib

English

If f is inducing, then s is Lindelöf iff f''s is Lindelöf.

Русский

Если f-индукция, то L Lindelöf для s эквивалентно L Lindelöf для f''s.

LaTeX

$$$(hf: IsInducing f) : IsLindelof s \leftrightarrow IsLindelof (f'' s)$$$

Lean4

/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is Lindelöf
  if and only if `s` is compact. -/
theorem isLindelof_iff {f : X → Y} (hf : IsInducing f) : IsLindelof s ↔ IsLindelof (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⟩

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