Theorems · Theorem · convex and discrete geometry

Convex.toCone_isLeast

Deprecated since 2026-03-30Mathlib marks this declaration as deprecated.

∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s),
  IsLeast {t | s ⊆ ↑t} (Convex.toCone s hs)

hs.toCone s is the least cone that includes s.

Defined in

Mathlib.Geometry.Convex.Cone.Basic

Cited by

2 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsStrictOrderedRingAddCommGroupModule