IsAcc — Mathlib

English

An ordinal o is an accumulation point of a set S if every neighborhood of o contains points of S arbitrarily close from below.

Русский

Ординал o является точкой накопления множества S, если каждый окрестности o содержит точки S, подходящие к o снизу.

LaTeX

$$IsAcc(o,S) is defined as AccPt o (𝓟 S).$$

Lean4

/-- An ordinal is an accumulation point of a set of ordinals if it is positive and there
are elements in the set arbitrarily close to the ordinal from below. -/
def IsAcc (o : Ordinal) (S : Set Ordinal) : Prop :=
  AccPt o (𝓟 S)

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