English
A set is absolutely convex if it is balanced with respect to 𝕜 and convex with respect to ℝ.
Русский
Множество абсолютно выпуклое, если оно сбалансировано по отношению к 𝕜 и выпукло по отношению к ℝ.
LaTeX
$$$AbsConvex(𝕜,s) \\;:=\\; Balanced 𝕜 s \\wedge Convex ℝ s$$$
Lean4
/-- A set is absolutely convex if it is balanced and convex. Mathlib's definition of `Convex`
requires the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` requires the
scalars to be a `SeminormedRing`. Mathlib doesn't currently have a concept of a semi-normed ordered
ring, so we define a set as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex
over `ℝ`. -/
def AbsConvex (s : Set E) : Prop :=
Balanced 𝕜 s ∧ Convex ℝ s
