α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = Ultrafilter.extend f (pure x)
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = Ultrafilter.extend f (pure x)
skip
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x

α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ f x = Ultrafilter.extend f (pure x)
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = Ultrafilter.extend f (pure x)
trans f x
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ f x = Ultrafilter.extend f (pure x)

α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x

α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ f x = Ultrafilter.extend f (pure x)
swap
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f (pure x) = f x

α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ f x = Ultrafilter.extend f (pure x)

α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
symm
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ ↑(pure x) ≤ 𝓝 x

α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ ↑u ≤ 𝓝 x
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f (pure x) = f x

α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
all_goals refine' ultrafilter_extend_eq_iff.mpr (le_trans (map_mono _) (hf.tendsto _))
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ ↑u ≤ 𝓝 x
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
refine' ultrafilter_extend_eq_iff.mpr (le_trans (map_mono _) (hf.tendsto _))
no goals
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ ↑(pure x) ≤ 𝓝 x
apply pure_le_nhds
no goals
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ ↑u ≤ 𝓝 x
exact ux