preStoneCechUnit — Mathlib

English

The natural map α → PreStoneCech α is given by sending x to the equivalence class of pure x.

Русский

Естественное отображение x ↦ эквивалентный класс чистого x в PreStoneCech α.

LaTeX

$$$preStoneCechUnit\; x = \operatorname{Quot.mk}\_\; (\mathrm{pure}\ x)$$$

Lean4

/-- The natural map from α to its pre-Stone-Čech compactification. -/
def preStoneCechUnit (x : α) : PreStoneCech α :=
  Quot.mk _ (pure x : Ultrafilter α)

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