English
If hf is Cauchy and hm makes the comap of the uniformity comparable to α, then comap m f is Cauchy for any nonempty comap.
Русский
Если hf — Коши и hm обеспечивает сравнимость комап равномерности β с α, то при любом непустом comap f фильтр становится Коши.
LaTeX
$$$ \text{Cauchy}(f) \land (\text{comap } m\, f) \text{ непрерывная по } α \Rightarrow \text{Cauchy}(\text{comap } m\, f)$$$
Lean4
nonrec theorem comap [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f)
(hm : comap (fun p : α × α => (m p.1, m p.2)) (𝓤 β) ≤ 𝓤 α) [NeBot (comap m f)] : Cauchy (comap m f) :=
⟨‹_›,
calc
comap m f ×ˢ comap m f = comap (Prod.map m m) (f ×ˢ f) := prod_comap_comap_eq
_ ≤ comap (Prod.map m m) (𝓤 β) := (comap_mono hf.right)
_ ≤ 𝓤 α := hm⟩
