English
If m: β → α is IsUniformInducing with dense range, and for every Cauchy filter on β there exists a limit in α, then α is complete.
Русский
Если m: β → α имеет свойство IsUniformInducing с плотным образом образа, и для каждого Cauchy-фильтра на β существует предел в α, тогда α полно.
LaTeX
$$$\text{If } m:\beta \to \alpha \text{ isIsUniformInducing with dense range and }\forall f (\text{Cauchy } f)\;\exists x\in \alpha:\; m_*f \to x, \text{ then } \CompleteSpace(\alpha).$$$
Lean4
theorem completeSpace_extension {m : β → α} (hm : IsUniformInducing m) (dense : DenseRange m)
(h : ∀ f : Filter β, Cauchy f → ∃ x : α, map m f ≤ 𝓝 x) : CompleteSpace α :=
⟨fun {f : Filter α} (hf : Cauchy f) =>
let p : Set (α × α) → Set α → Set α := fun s t => {y : α | ∃ x : α, x ∈ t ∧ (x, y) ∈ s}
let g := (𝓤 α).lift fun s => f.lift' (p s)
have mp₀ : Monotone p := fun _ _ h _ _ ⟨x, xs, xa⟩ => ⟨x, xs, h xa⟩
have mp₁ : ∀ {s}, Monotone (p s) := fun h _ ⟨y, ya, yxs⟩ => ⟨y, h ya, yxs⟩
have : f ≤ g :=
le_iInf₂ fun _ hs =>
le_iInf₂ fun _ ht => le_principal_iff.mpr <| mem_of_superset ht fun x hx => ⟨x, hx, refl_mem_uniformity hs⟩
have : NeBot g := hf.left.mono this
have : NeBot (comap m g) :=
comap_neBot fun _ ht =>
let ⟨t', ht', ht_mem⟩ := (mem_lift_sets <| monotone_lift' monotone_const mp₀).mp ht
let ⟨_, ht'', ht'_sub⟩ := (mem_lift'_sets mp₁).mp ht_mem
let ⟨x, hx⟩ := hf.left.nonempty_of_mem ht''
have h₀ : NeBot (𝓝[range m] x) := dense.nhdsWithin_neBot x
have h₁ : {y | (x, y) ∈ t'} ∈ 𝓝[range m] x := @mem_inf_of_left α (𝓝 x) (𝓟 (range m)) _ <| mem_nhds_left x ht'
have h₂ : range m ∈ 𝓝[range m] x := @mem_inf_of_right α (𝓝 x) (𝓟 (range m)) _ <| Subset.refl _
have : {y | (x, y) ∈ t'} ∩ range m ∈ 𝓝[range m] x := @inter_mem α (𝓝[range m] x) _ _ h₁ h₂
let ⟨_, xyt', b, b_eq⟩ := h₀.nonempty_of_mem this
⟨b, b_eq.symm ▸ ht'_sub ⟨x, hx, xyt'⟩⟩
have : Cauchy g :=
⟨‹NeBot g›, fun _ hs =>
let ⟨s₁, hs₁, comp_s₁⟩ := comp_mem_uniformity_sets hs
let ⟨s₂, hs₂, comp_s₂⟩ := comp_mem_uniformity_sets hs₁
let ⟨t, ht, (prod_t : t ×ˢ t ⊆ s₂)⟩ := mem_prod_same_iff.mp (hf.right hs₂)
have hg₁ : p (preimage Prod.swap s₁) t ∈ g := mem_lift (symm_le_uniformity hs₁) <| @mem_lift' α α f _ t ht
have hg₂ : p s₂ t ∈ g := mem_lift hs₂ <| @mem_lift' α α f _ t ht
have hg : p (Prod.swap ⁻¹' s₁) t ×ˢ p s₂ t ∈ g ×ˢ g := @prod_mem_prod α α _ _ g g hg₁ hg₂
(g ×ˢ g).sets_of_superset hg fun ⟨_, _⟩ ⟨⟨c₁, c₁t, hc₁⟩, ⟨c₂, c₂t, hc₂⟩⟩ =>
have : (c₁, c₂) ∈ t ×ˢ t := ⟨c₁t, c₂t⟩
comp_s₁ <| prodMk_mem_compRel hc₁ <| comp_s₂ <| prodMk_mem_compRel (prod_t this) hc₂⟩
have : Cauchy (Filter.comap m g) := ‹Cauchy g›.comap' (le_of_eq hm.comap_uniformity) ‹_›
let ⟨x, (hx : map m (Filter.comap m g) ≤ 𝓝 x)⟩ := h _ this
have : ClusterPt x (map m (Filter.comap m g)) := (le_nhds_iff_adhp_of_cauchy (this.map hm.uniformContinuous)).mp hx
have : ClusterPt x g := this.mono map_comap_le
⟨x,
calc
f ≤ g := by assumption
_ ≤ 𝓝 x := le_nhds_of_cauchy_adhp ‹Cauchy g› this⟩⟩
