isCompact_preimage — Mathlib

English

For an inducing map f, IsCompact s is equivalent to IsCompact (f '' s).

Русский

Для отображения, являющегося инфуцированием, компактность множества сохраняется через образ.

LaTeX

$$IsCompact(s) ↔ IsCompact(f''s) (for hf : IsInducing f)$$

Lean4

/-- The preimage of a compact set under an inducing map is a compact set. -/
theorem isCompact_preimage (hf : IsInducing f) (hf' : IsClosed (range f)) {K : Set Y} (hK : IsCompact K) :
    IsCompact (f ⁻¹' K) := by
  replace hK := hK.inter_right hf'
  rwa [hf.isCompact_iff, image_preimage_eq_inter_range]

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