cauchy_map_iff — Mathlib

English

Equivalent formulation of Cauchy preservation under uniform embeddings via map and comap relations.

Русский

Эквивалентная формулировка сохранения Коши через отображения и комапы.

LaTeX

$$$\\text{Cauchy}(\\text{map } f F) \\iff \\text{Cauchy } F$$$

Lean4

theorem cauchy_map_iff {f : α → β} (hf : IsUniformInducing f) {F : Filter α} : Cauchy (map f F) ↔ Cauchy F := by
  simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap, ← hf.comap_uniformity]

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