finite

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#BddAbove.finite

English

If a set is bounded above in a locally finite order with a top, then it is finite.

Русский

Если множество ограничено сверху в локально конечном порядке с верхней границей, то оно конечное.

LaTeX

$$BddAbove s \rightarrow s.Finite$$

Lean4

theorem _root_.BddAbove.finite {s : Set α} (hs : BddAbove s) : s.Finite :=
  hs.dual.finite

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

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

Разделы

Аффилиация

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