induced_topology_pure — Mathlib

English

The map pure induces on α the discrete topology: the induced topology equals the bottom/topological structure ⊥, i.e., discrete.

Русский

Отображение pure индуцирует на α дискретную топологию: индуцированная топология равна ⊥ (дискретизация).

LaTeX

$$$TopologicalSpace.induced\left(\mathrm{pure}: α \to Ultrafilter\ α\right) Ultrafilter.topologicalSpace = ⊥$$$

Lean4

/-- The map `pure : α → Ultrafilter α` induces on `α` the discrete topology. -/
theorem induced_topology_pure : TopologicalSpace.induced (pure : α → Ultrafilter α) Ultrafilter.topologicalSpace = ⊥ :=
  by
  apply eq_bot_of_singletons_open
  intro x
  use {u : Ultrafilter α | { x } ∈ u}, ultrafilter_isOpen_basic _
  simp

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