IsCompact — Mathlib

English

A set s is compact if for every nontrivial filter f with f ≤ 𝓟 s there exists x ∈ s with ClusterPt x f.

Русский

Множество s компактно, если для каждого ненулевого фильтра f, удовлетворяющего f ≤ 𝓟 s, существует x ∈ s, такой что x является кластерной точкой f.

LaTeX

$$$IsCompact(s) := \forall ⦃f⦄ [NeBot f], f \leq 𝓟 s \to \exists x \in s, ClusterPt x f$$$

Lean4

/-- A set `s` is compact if for every nontrivial filter `f` that contains `s`,
there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`. -/
def IsCompact (s : Set X) :=
  ∀ ⦃f⦄ [NeBot f], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f

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