not_bddBelow

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Set.Infinite.not_bddBelow

English

An infinite set cannot be bounded below in the given order structure.

Русский

Бесконечное множество не может иметь нижнюю границу в данной структуре порядка.

LaTeX

$$Set.Infinite.not_bddBelow$$

Lean4

theorem _root_.Set.Infinite.not_bddBelow {s : Set α} : s.Infinite → ¬BddBelow s :=
  mt BddBelow.finite

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

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

Разделы

Аффилиация

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