infinite_of_not_bddAbove

Mathlib.Data.Set.Finite.Lattice

URI: https://scilib.ai/kg/mathlib#Set.infinite_of_not_bddAbove

English

If a set is not bounded above, then it is infinite.

Русский

Если множество не ограничено сверху, то оно бесконечно.

LaTeX

$$$(\lnot BddAbove\ s) \Rightarrow s\text{ Infinite}$$$

Lean4

theorem infinite_of_not_bddAbove : ¬BddAbove s → s.Infinite :=
  mt Finite.bddAbove

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

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

Разделы

Аффилиация

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