zero_mem_absConvexHull — Mathlib

English

If s is nonempty, then 0 belongs to the absConvexHull of s.

Русский

Если s непусто, то 0 принадлежит absConvexHull(s).

LaTeX

$$$0 \\in \\operatorname{absConvexHull}_{( )}(s)$$$

Lean4

theorem zero_mem_absConvexHull {s : Set E} [SeminormedRing 𝕜] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [Nonempty s] :
    0 ∈ absConvexHull 𝕜 s :=
  balanced_absConvexHull.zero_mem (Nonempty.mono subset_absConvexHull Set.Nonempty.of_subtype)

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