instCompactSpace_coe — Mathlib

English

There is a canonical instance that the type underlying stdSimplex Real ι is a compact space.

Русский

Существует канонический экземпляр, что множество, лежащее в основе stdSimplex Real ι, является компактным пространством.

LaTeX

$$$\text{instCompactSpace_coe} : \text{CompactSpace} \; (\mathrm{stdSimplex}_{\mathbb{R}}(\iota))$$$

Lean4

instance instCompactSpace_coe : CompactSpace ↥(stdSimplex ℝ ι) :=
  isCompact_iff_compactSpace.mp <| isCompact_stdSimplex _

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