totallyBounded_preimage — Mathlib

English

If f is IsUniformInducing and s is totally bounded, then the preimage f^{-1}(s) is totally bounded.

Русский

Если f — IsUniformInducing и s полностью ограничено, то предобраз f^{-1}(s) тоже полностью ограничено.

LaTeX

$$$\text{If } f:\alpha \to \beta\text{ is IsUniformInducing and } s\subseteq \beta\text{ is totally bounded, then } f^{-1}(s)\text{ is totally bounded.}$$$

Lean4

theorem totallyBounded_preimage {f : α → β} {s : Set β} (hf : IsUniformInducing f) (hs : TotallyBounded s) :
    TotallyBounded (f ⁻¹' s) :=
  (totallyBounded_image_iff hf).1 <| hs.subset <| image_preimage_subset ..

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