α : Type u
β : Type v
inst✝ : UniformSpace α
l : Filter α
h : Cauchy l
this : NeBot l
⊢ Cauchy ↑(Ultrafilter.of l)
α : Type u
β : Type v
inst✝ : UniformSpace α
l : Filter α
h : Cauchy l
⊢ Cauchy ↑(Ultrafilter.of l)
haveI := h.1
α : Type u
β : Type v
inst✝ : UniformSpace α
l : Filter α
h : Cauchy l
this✝ : NeBot l
this : ↑(Ultrafilter.of l) ≤ l
⊢ Cauchy ↑(Ultrafilter.of l)
α : Type u
β : Type v
inst✝ : UniformSpace α
l : Filter α
h : Cauchy l
this : NeBot l
⊢ Cauchy ↑(Ultrafilter.of l)
have := Ultrafilter.of_le l
no goals
α : Type u
β : Type v
inst✝ : UniformSpace α
l : Filter α
h : Cauchy l
this✝ : NeBot l
this : ↑(Ultrafilter.of l) ≤ l
⊢ Cauchy ↑(Ultrafilter.of l)
exact ⟨Ultrafilter.neBot _, (Filter.prod_mono this this).trans h.2⟩