toCone_eq_sInf — Mathlib

English

The cone generated by s is the infimum of all cones that contain s; i.e., hs.toCone s = sInf { t : ConvexCone 𝕜 M | s ⊆ t }.

Русский

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

LaTeX

$$hs.toCone s = sInf { t : ConvexCone 𝕜 M | s ⊆ t }$$

Lean4

theorem toCone_eq_sInf : hs.toCone s = sInf {t : ConvexCone 𝕜 M | s ⊆ t} :=
  hs.toCone_isLeast.isGLB.sInf_eq.symm

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