atBot_atTop_le_cocompact — Mathlib

English

In a NoMinOrder NoMaxOrder space with OrderClosedTopology, the join of bottom and top is contained in the cocompact filter: atBot ⊔ atTop ≤ cocompact α.

Русский

В пространстве без минимума и без максимума с OrderClosedTopology объединение нижнего и верхнего концов входит в коккомпактный фильтр: atBot ⊔ atTop ≤ cocompact α.

LaTeX

$$$\text{atBot} \sqcup \text{atTop} \le \text{cocompact}(\alpha)$$$

Lean4

theorem atBot_atTop_le_cocompact [NoMinOrder α] [NoMaxOrder α] [OrderClosedTopology α] : atBot ⊔ atTop ≤ cocompact α :=
  sup_le atBot_le_cocompact atTop_le_cocompact

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