English
Let α and β be spaces with uniform structures. Let f be a filter on β and m: α → β a map. If f is Cauchy, the pullback of the β-uniformity along m×m is dominated by the α-uniformity, and comap m f is nontrivial, then comap m f is Cauchy on α.
Русский
Пусть α и β — множества с униформностями, f — фильтр на β, и m: α → β — отображение. Если f является компактно-Коши (когда его изучают через униформности), тождественное вложение униформности β через m×m доминируется над униформностью α, и comap_m f ненулевой, тогда comap_m f является Коши-фильтром на α.
LaTeX
$$$\\text{If } f \\text{ is Cauchy on } β,\\, \\operatorname{comap}_{(m\\times m)}(\\mathcal{U}_β) \\le \\mathcal{U}_α,\\, \\operatorname{NeBot}(\\operatorname{comap}_m f),\\text{ then } \\operatorname{Cauchy}(\\operatorname{comap}_m f).$$$
Lean4
theorem comap' [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f)
(hm : Filter.comap (fun p : α × α => (m p.1, m p.2)) (𝓤 β) ≤ 𝓤 α) (_ : NeBot (Filter.comap m f)) :
Cauchy (Filter.comap m f) :=
hf.comap hm
