pos

Mathlib.SetTheory.Ordinal.Topology

URI: https://scilib.ai/kg/mathlib#Ordinal.IsAcc.pos

English

If o is an accumulation point of S, then o is strictly positive.

Русский

Если o является точкой накопления S, то o строго положительно.

LaTeX

$$pos {o} {S} (h : o.IsAcc S) : 0 < o$$

Lean4

theorem pos {o : Ordinal} {S : Set Ordinal} (h : o.IsAcc S) : 0 < o :=
  Ordinal.pos_iff_ne_zero.mpr ((isAcc_iff _ _).mp h).1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru