subset_hull

Mathlib.Geometry.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#ConvexCone.subset_hull

English

Every set is contained in its hull.

Русский

Каждое множество содержится в своей оболочке.

LaTeX

$$s ⊆ hull R s$$

Lean4

theorem subset_hull : s ⊆ hull R s := by simp [hull]

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

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

Разделы

Аффилиация

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