isClosed_stdSimplex — Mathlib

English

The real-valued standard simplex stdSimplex Real ι is a closed set for finite ι.

Русский

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

LaTeX

$$$\mathrm{IsClosed}(\mathrm{stdSimplex}_{\mathbb{R}}(\iota))$$$

Lean4

/-- `stdSimplex ℝ ι` is closed. -/
theorem isClosed_stdSimplex : IsClosed (stdSimplex ℝ ι) :=
  (stdSimplex_eq_inter ℝ ι).symm ▸
    IsClosed.inter (isClosed_iInter fun i => isClosed_le continuous_const (continuous_apply i))
      (isClosed_eq (continuous_finset_sum _ fun x _ => continuous_apply x) continuous_const)

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