convexAddSubmonoid — Mathlib

English

The coe of convexAddSubmonoid equals the set of convex sets.

Русский

Ковыражение convexAddSubmonoid равно множеству выпуклых множеств.

LaTeX

$$$↑(convexAddSubmonoid 𝕜 E) = \{ s : Set E \mid Convex 𝕜 s \}$$$

Lean4

/-- The convex sets form an additive submonoid under pointwise addition. -/
noncomputable def convexAddSubmonoid : AddSubmonoid (Set E)
    where
  carrier := {s : Set E | Convex 𝕜 s}
  zero_mem' := convex_zero
  add_mem' := Convex.add

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