subset_toCone

Mathlib.Geometry.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#Convex.subset_toCone

English

If s is convex, then s is contained in the cone generated by s: s ⊆ hs.toCone s.

Русский

Если s выпукло, тогда s содержится в конусе, порождаемом s: s ⊆ hs.toCone s.

LaTeX

$$$ s \subseteq hs.toCone s $$$

Lean4

theorem subset_toCone : s ⊆ hs.toCone s := fun x hx => hs.mem_toCone'.2 ⟨1, zero_lt_one, by rwa [one_smul]⟩

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

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

Разделы

Аффилиация

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