case mp.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : CauchyFilter α
⊢ Nonempty α

case mpr.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : α
⊢ Nonempty (CauchyFilter α)
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ Nonempty (CauchyFilter α) ↔ Nonempty α
constructor <;> rintro ⟨c⟩
case mp.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
⊢ Nonempty α
case mp.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : CauchyFilter α
⊢ Nonempty α
have := eq_univ_iff_forall.1 denseEmbedding_pureCauchy.toDenseInducing.closure_range c
case mp.intro.intro.intro.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
w✝ : CauchyFilter α
left✝ : w✝ ∈ univ
a : α
h✝ : pureCauchy a = w✝
⊢ Nonempty α
case mp.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
⊢ Nonempty α
obtain ⟨_, ⟨_, a, _⟩⟩ := mem_closure_iff.1 this _ isOpen_univ trivial
no goals
case mp.intro.intro.intro.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
w✝ : CauchyFilter α
left✝ : w✝ ∈ univ
a : α
h✝ : pureCauchy a = w✝
⊢ Nonempty α
exact ⟨a⟩
no goals
case mpr.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : α
⊢ Nonempty (CauchyFilter α)
exact ⟨pureCauchy c⟩