cauchy_comap_uniformSpace — Mathlib

English

If the comap of a uniformity via m is below the base, Cauchy of comap f f implies Cauchy of map.

Русский

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

LaTeX

$$$ Cauchy(\text{uniformSpace} := comap f\, u)\; l \iff Cauchy(\text{map } f\, l) $$$

Lean4

theorem cauchy_comap_uniformSpace {u : UniformSpace β} {α} {f : α → β} {l : Filter α} :
    Cauchy (uniformSpace := comap f u) l ↔ Cauchy (map f l) :=
  by
  simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap]
  rfl

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