English
For any b, c in α-space, Ultrafilter.extend f b = c iff the filter map f of b is ≤ nhds c.
Русский
Для любых b, c верно: Ultrafilter.extend f b = c тогда и только тогда, когда \(b.map f\) ≤ nhds c.
LaTeX
$$$Ultrafilter\\.extend\\ f\\ b = c \\iff ↑(b.map f) \\le 𝓝 c$$$
Lean4
/-- The value of `Ultrafilter.extend f` on an ultrafilter `b` is the
unique limit of the ultrafilter `b.map f` in `γ`. -/
theorem ultrafilter_extend_eq_iff {f : α → γ} {b : Ultrafilter α} {c : γ} :
Ultrafilter.extend f b = c ↔ ↑(b.map f) ≤ 𝓝 c :=
⟨fun h ↦ by
-- Write b as an ultrafilter limit of pure ultrafilters, and use
-- the facts that ultrafilter.extend is a continuous extension of f.
let b' : Ultrafilter (Ultrafilter α) := b.map pure
have t : ↑b' ≤ 𝓝 b := ultrafilter_converges_iff.mpr (bind_pure _).symm
rw [← h]
have := (continuous_ultrafilter_extend f).tendsto b
refine le_trans ?_ (le_trans (map_mono t) this)
change _ ≤ map (Ultrafilter.extend f ∘ pure) ↑b
rw [ultrafilter_extend_extends]
exact le_rfl, fun h ↦
let _ : TopologicalSpace α := ⊥
isDenseInducing_pure.extend_eq_of_tendsto (le_trans (map_mono (ultrafilter_comap_pure_nhds _)) h)⟩
