denseRange_pure — Mathlib

English

The range of the map pure: α → Ultrafilter α is dense in Ultrafilter α.

Русский

Область значений отображения pure: α → Ultrafilter α плотна в Ultrafilter α.

LaTeX

$$$DenseRange\big(\mathrm{pure}: α \to Ultrafilter\ α\big)$$$

Lean4

/-- The range of `pure : α → Ultrafilter α` is dense in `Ultrafilter α`. -/
theorem denseRange_pure : DenseRange (pure : α → Ultrafilter α) := fun x ↦
  mem_closure_iff_ultrafilter.mpr ⟨x.map pure, range_mem_map, ultrafilter_converges_iff.mpr (bind_pure x).symm⟩

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