isCobounded_top

Mathlib.Order.Filter.IsBounded

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

English

IsCobounded r ⊤ is equivalent to the nonemptiness of the type A (i.e., α is nonempty).

Русский

IsCobounded r топ эквивалентно ненулевости множества атомов; здесь α не пуст.

LaTeX

$$$IsCobounded\ r\ \top \ \Leftrightarrow\ Nonempty\ α.$$$

Lean4

theorem isCobounded_top : IsCobounded r ⊤ ↔ Nonempty α := by simp +contextual [IsCobounded, exists_true_iff_nonempty]

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

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

Разделы

Аффилиация

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