isBounded_le_atBot

Mathlib.Order.Filter.IsBounded

URI: https://scilib.ai/kg/mathlib#Filter.isBounded_le_atBot

English

For any nonempty α with a preorder, the atBot filter is bounded above by ≤.

Русский

Для непустого множества α с полным порядком фильтр atBot ограничен сверху по ≤.

LaTeX

$$$\text{isBounded_le_atBot}: (atBot : Filter \alpha).IsBounded(\le)$$$

Lean4

theorem isBounded_le_atBot : (atBot : Filter α).IsBounded (· ≤ ·) :=
  ‹Nonempty α›.elim fun a => ⟨a, eventually_le_atBot _⟩

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

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

Разделы

Аффилиация

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