map — Mathlib

English

If m is UniformContinuous, then Cauchy f implies Cauchy (map m f).

Русский

Если m непрерывно-однородно непрерывно по равномерности, то Коши-фильтр f влечет за собой Коши-образ map m f.

LaTeX

$$$ \text{Cauchy}(f) \rightarrow \text{UniformContinuous}(m) \rightarrow \text{Cauchy}(\text{map } m f)$$$

Lean4

nonrec theorem map [UniformSpace β] {f : Filter α} {m : α → β} (hf : Cauchy f) (hm : UniformContinuous m) :
    Cauchy (map m f) :=
  ⟨hf.1.map _,
    calc
      map m f ×ˢ map m f = map (Prod.map m m) (f ×ˢ f) := Filter.prod_map_map_eq
      _ ≤ Filter.map (Prod.map m m) (𝓤 α) := (map_mono hf.right)
      _ ≤ 𝓤 β := hm⟩

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