convex_parallelepiped

Mathlib.MeasureTheory.Measure.Haar.OfBasis

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

← MathLib Explorer

English

Every parallelepiped is a convex set.

Русский

Каждый параллелепипед является выпуклым множеством.

LaTeX

$$$\\mathrm{parallelepiped}(v) \\subseteq \\operatorname{ConvexHull}(\\mathbb{R})$.$$

Lean4

theorem convex_parallelepiped (v : ι → E) : Convex ℝ (parallelepiped v) :=
  by
  rw [parallelepiped_eq_sum_segment]
  exact convex_sum _ fun _i _hi => convex_segment _ _

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

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

Разделы

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

Аффилиация

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