instCompactIccSpaceOrderDual — Mathlib

English

If α has CompactIccSpace, then its order dual α^o also has CompactIccSpace.

Русский

Если у α есть CompactIccSpace, то у α^o тоже есть CompactIccSpace.

LaTeX

$$∀ {α}, [CompactIccSpace α] → CompactIccSpace (OrderDual α)$$

Lean4

instance [TopologicalSpace α] [Preorder α] [CompactIccSpace α] : CompactIccSpace (αᵒᵈ) where
  isCompact_Icc := by
    intro a b
    convert isCompact_Icc (α := α) (a := b) (b := a) using 1
    exact Icc_toDual (α := α)

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