IsClosedBelow — Mathlib

English

A set S is closed below an ordinal o if it contains all accumulation points of S that lie below o.

Русский

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

LaTeX

$$IsClosedBelow(S,o) is defined as IsClosed (Iio o ↓∩ S).$$

Lean4

/-- A set of ordinals is closed below an ordinal if it contains all of
its accumulation points below the ordinal. -/
def IsClosedBelow (S : Set Ordinal) (o : Ordinal) : Prop :=
  IsClosed (Iio o ↓∩ S)

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