unbounded_of_isEmpty

Mathlib.Order.RelClasses

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

English

If α is an empty type, then for any r, the set s is unbounded.

Русский

Если множество α пусто, то любое множество s является неограниченным по отношению к r.

LaTeX

$$Unbounded(r,s)$$

Lean4

theorem unbounded_of_isEmpty [IsEmpty α] {r : α → α → Prop} (s : Set α) : Unbounded r s :=
  isEmptyElim

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

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

Разделы

Аффилиация

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