isDenseInducing_pure — Mathlib

English

The map pure is a dense inducing from α into Ultrafilter α.

Русский

Отображение pure является плотной-индукцией из α в Ultrafilter α.

LaTeX

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

Lean4

/-- `pure : α → Ultrafilter α` defines a dense inducing of `α` in `Ultrafilter α`. -/
theorem isDenseInducing_pure : @IsDenseInducing _ _ ⊥ _ (pure : α → Ultrafilter α) :=
  letI : TopologicalSpace α := ⊥
  ⟨⟨induced_topology_pure.symm⟩, denseRange_pure⟩
    -- The following refined version will never be used

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