English
Let s be a subset of a vector space M and hs be a convex set in s. Then an element x belongs to the cone generated by s, hs.toCone s, if and only if there exist a positive scalar c ∈ 𝕜 and a point y ∈ s with x = c · y.
Русский
Пусть s ⊆ M и hs⊆M выпукло. Тогда элемент x принадлежит конусу, порождаемому s, если и только если существует положительный скаляр c ∈ 𝕜 и точка y ∈ s такая, что x = c y.
LaTeX
$$$ x \in hs.toCone s \iff \exists c \; (0 < c) \wedge \exists y \in s, c \cdot y = x $$$
Lean4
theorem mem_toCone : x ∈ hs.toCone s ↔ ∃ c : 𝕜, 0 < c ∧ ∃ y ∈ s, c • y = x := by
simp only [toCone, ConvexCone.mem_mk, mem_iUnion, mem_smul_set, eq_comm, exists_prop]
