English
The space of Cauchy filters on α is a complete space.
Русский
Пространство фильтров Коши над α является полным пространством.
LaTeX
$$$\\text{CompleteSpace}(\\mathrm{CauchyFilter}(\\alpha))$$$
Lean4
instance : CompleteSpace (CauchyFilter α) :=
completeSpace_extension isUniformInducing_pureCauchy denseRange_pureCauchy fun f hf =>
let f' : CauchyFilter α := ⟨f, hf⟩
have : map pureCauchy f ≤ (𝓤 <| CauchyFilter α).lift' (preimage (Prod.mk f')) :=
le_lift'.2 fun _ hs =>
let ⟨t, ht₁, ht₂⟩ := (mem_lift'_sets monotone_gen).mp hs
let ⟨t', ht', (h : t' ×ˢ t' ⊆ t)⟩ := mem_prod_same_iff.mp (hf.right ht₁)
have : t' ⊆ {y : α | (f', pureCauchy y) ∈ gen t} := fun x hx =>
(f ×ˢ pure x).sets_of_superset (prod_mem_prod ht' hx) h
f.sets_of_superset ht' <| Subset.trans this (preimage_mono ht₂)
⟨f', by simpa [nhds_eq_uniformity]⟩
