isDenseEmbedding_pure — Mathlib

English

The map pure is a dense embedding of α into Ultrafilter α.

Русский

Отображение pure является плотным вложением α в Ultrafilter α.

LaTeX

$$$IsDenseEmbedding\left(\mathrm{pure}: α \to Ultrafilter\ α\right)$$$

Lean4

/-- `pure : α → Ultrafilter α` defines a dense embedding of `α` in `Ultrafilter α`. -/
theorem isDenseEmbedding_pure : @IsDenseEmbedding _ _ ⊥ _ (pure : α → Ultrafilter α) :=
  letI : TopologicalSpace α := ⊥
  { isDenseInducing_pure with injective := Ultrafilter.pure_injective }

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