PreStoneCech — Mathlib

English

PreStoneCech α is the auxiliary quotient type formed by Ultrafilter α under the relation ∼ where F ∼ G if ∃ x with F ≤ 𝓝 x and G ≤ 𝓝 x.

Русский

PreStoneCech α — вспомогательный тип-окончание как отношение эквивалентности между ультрафильтрами, где F ∼ G ⇔∃ x, F ≤ 𝓝 x и G ≤ 𝓝 x.

LaTeX

$$$PreStoneCech\ α := Quot\;\big(\lambda F\,G, \; ∃ x, (F:Filter\ α) ≤ 𝓝 x ∧ (G:Filter\ α) ≤ 𝓝 x\big)$$$

Lean4

/-- Auxiliary construction towards the Stone-Čech compactification of a topological space.
It should not be used after the Stone-Čech compactification is constructed. -/
def PreStoneCech : Type u :=
  Quot fun F G : Ultrafilter α ↦ ∃ x, (F : Filter α) ≤ 𝓝 x ∧ (G : Filter α) ≤ 𝓝 x

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