α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
have : (g.map pure).toFilter ≤ 𝓝 g := by
  rw [ultrafilter_converges_iff]
  exact (bind_pure _).symm
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
this : ↑(Ultrafilter.map stoneCechUnit g) ≤ 𝓝 (Quotient.mk (stoneCechSetoid α) g)
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
have : (g.map stoneCechUnit : Filter (StoneCech α)) ≤ 𝓝 ⟦g⟧ :=
  continuousAt_iff_ultrafilter.mp (continuous_quotient_mk'.tendsto g) _ this
no goals
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
this : ↑(Ultrafilter.map stoneCechUnit g) ≤ 𝓝 (Quotient.mk (stoneCechSetoid α) g)
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
rwa [show ⟦g⟧ = ⟦pure x⟧ from Quotient.sound <| convergent_eqv_pure gx] at this
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ g = joinM (Ultrafilter.map pure g)
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ ↑(Ultrafilter.map pure g) ≤ 𝓝 g
rw [ultrafilter_converges_iff]
no goals
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ g = joinM (Ultrafilter.map pure g)
exact (bind_pure _).symm