toCone_isLeast — Mathlib

English

For a convex s, the cone hs.toCone s is the least cone containing s; equivalently, it is the smallest cone that contains s.

Русский

Для выпуклого множества s конус hs.toCone s является наименьшим конусом, содержащим s; то есть наименьшим cone, который содержит s.

LaTeX

$$Is Least ( { t : ConvexCone 𝕜 M | s ⊆ t } ) ( hs.toCone s )$$

Lean4

/-- `hs.toCone s` is the least cone that includes `s`. -/
theorem toCone_isLeast : IsLeast {t : ConvexCone 𝕜 M | s ⊆ t} (hs.toCone s) :=
  by
  refine ⟨hs.subset_toCone, fun t ht x hx => ?_⟩
  rcases hs.mem_toCone.1 hx with ⟨c, hc, y, hy, rfl⟩
  exact t.smul_mem hc (ht hy)

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