English
A balance is equivalent to closure under negation for convex sets.
Русский
Балансированность эквивалентна замыканию по отрицательному элементу для выпуклых множеств.
LaTeX
$$$\\text{Convex Real } s \Rightarrow (\\text{Balanced Real } s \\Longleftrightarrow \\forall x \\in s, -x \\in s)$$$
Lean4
theorem balanced_iff_neg_mem (hs : Convex ℝ s) : Balanced ℝ s ↔ ∀ ⦃x⦄, x ∈ s → -x ∈ s :=
by
refine ⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => ?_⟩
rw [Real.norm_eq_abs, abs_le] at ha
rw [show a = -((1 - a) / 2) + (a - -1) / 2 by ring, add_smul, neg_smul, ← smul_neg]
exact
hs (h hx) hx (div_nonneg (sub_nonneg_of_le ha.2) zero_le_two) (div_nonneg (sub_nonneg_of_le ha.1) zero_le_two)
(by ring)
