bounded_stdSimplex

Mathlib.Analysis.Convex.StdSimplex

URI: https://scilib.ai/kg/mathlib#bounded_stdSimplex

← MathLib Explorer

English

The standard simplex stdSimplex 𝕜 ι is bounded when ι is finite.

Русский

Стандартный симплекс stdSimplex 𝕜 ι ограничен, когда ι конечно.

LaTeX

$$$\mathrm{IsBounded}(\mathrm{stdSimplex}_{\mathbb{k}}(\iota))$$$

Lean4

/-- `stdSimplex ℝ ι` is bounded. -/
theorem bounded_stdSimplex : IsBounded (stdSimplex ℝ ι) :=
  (Metric.isBounded_iff_subset_closedBall 0).2 ⟨1, stdSimplex_subset_closedBall⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru