English
The range of pureCauchy: α → CauchyFilter α is dense in CauchyFilter α.
Русский
Образ pureCauchy: α → CauchyFilter α является плотным в CauchyFilter α.
LaTeX
$$$\\operatorname{DenseRange}(\\mathrm{pureCauchy})$$$
Lean4
theorem denseRange_pureCauchy : DenseRange (pureCauchy : α → CauchyFilter α) := fun f =>
by
have h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y : α, (f, pureCauchy y) ∈ s := fun s hs =>
let ⟨t'', ht''₁, (ht''₂ : gen t'' ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs
let ⟨t', ht'₁, ht'₂⟩ := comp_mem_uniformity_sets ht''₁
have : t' ∈ f.val ×ˢ f.val := f.property.right ht'₁
let ⟨t, ht, (h : t ×ˢ t ⊆ t')⟩ := mem_prod_same_iff.mp this
let ⟨x, (hx : x ∈ t)⟩ := f.property.left.nonempty_of_mem ht
have : t'' ∈ f.val ×ˢ pure x :=
mem_prod_iff.mpr
⟨t, ht, {y : α | (x, y) ∈ t'}, h <| mk_mem_prod hx hx, fun ⟨a, b⟩ ⟨(h₁ : a ∈ t), (h₂ : (x, b) ∈ t')⟩ =>
ht'₂ <| prodMk_mem_compRel (@h (a, x) ⟨h₁, hx⟩) h₂⟩
⟨x, ht''₂ <| by dsimp [gen]; exact this⟩
simp only [closure_eq_cluster_pts, ClusterPt, nhds_eq_uniformity, lift'_inf_principal_eq,
Set.inter_comm _ (range pureCauchy), mem_setOf_eq]
refine (lift'_neBot_iff ?_).mpr (fun s hs => ?_)
· exact monotone_const.inter monotone_preimage
· let ⟨y, hy⟩ := h_ex s hs
have : pureCauchy y ∈ range pureCauchy ∩ {y : CauchyFilter α | (f, y) ∈ s} := ⟨mem_range_self y, hy⟩
exact ⟨_, this⟩
