unbounded_le_univ

Mathlib.Order.Bounded

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

English

The universal set is unbounded for ≤ (under standard order assumptions).

Русский

Общее множество неограничено по ≤ (при обычных предпосылках порядка).

LaTeX

$$Unbounded(≤, Set.univ)$$

Lean4

theorem unbounded_le_univ [LE α] [NoTopOrder α] : Unbounded (· ≤ ·) (@Set.univ α) := fun a =>
  let ⟨b, hb⟩ := exists_not_le a
  ⟨b, ⟨⟩, hb⟩

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

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

Разделы

Аффилиация

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