mem_convexAddSubmonoid — Mathlib

English

The convex sets form an additive submonoid under pointwise addition.

Русский

Множество выпуклых подмножеств образует аддитивный подмоноид при точечной сложении.

LaTeX

$$$\emptyset \in convexAddSubmonoid 𝕜 E \land \forall s,t \in convexAddSubmonoid 𝕜 E,\ s+t \in convexAddSubmonoid 𝕜 E$$$

Lean4

@[simp]
theorem mem_convexAddSubmonoid {s : Set E} : s ∈ convexAddSubmonoid 𝕜 E ↔ Convex 𝕜 s :=
  Iff.rfl

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