coatomic_of_top_compact — Mathlib

English

If k is a compact element of α, then the interval set Iic(k) is coatomic as a sublattice.

Русский

Если k — компактный элемент α, то множество Iic(k) коатомно в качестве подпорядка.

LaTeX

$$$ \text{IsCoatomic}(\,\mathrm{Iic}(k)\,)$ given $k$ compact in α$$

Lean4

theorem coatomic_of_top_compact (h : IsCompactElement (⊤ : α)) : IsCoatomic α :=
  (@OrderIso.IicTop α _ _).isCoatomic_iff.mp (Iic_coatomic_of_compact_element h)

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