tendsto_pure_self — Mathlib

English

For any ultrafilter b on α, the map pure sends b toward itself in the ultrafilter topology: Tendsto pure b (𝓝 b).

Русский

Для любого ультрафильтра b на α отображение pure стремится к b в топологическом пространстве ультрафильтров: Tendsto pure b (𝓝 b).

LaTeX

$$$\operatorname{Tendsto}\,\mathrm{pure}\, b\; (𝓝 b)$$$

Lean4

@[simp]
theorem tendsto_pure_self (b : Ultrafilter α) : Tendsto pure b (𝓝 b) :=
  by
  rw [Tendsto, ← coe_map, ultrafilter_converges_iff]
  ext s
  change s ∈ b ↔ {t | s ∈ t} ∈ map pure b
  simp_rw [mem_map, preimage_setOf_eq, mem_pure, setOf_mem_eq]

Похожие утверждения