𝕜 : Type ?u.232896
𝕝 : Type ?u.232899
E : Type u_1
ι : Sort ?u.232905
κ : ι → Sort ?u.232910
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
𝕜 : Type ?u.232896
𝕝 : Type ?u.232899
E : Type u_1
ι : Sort ?u.232905
κ : ι → Sort ?u.232910
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
⊢ Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
refine' ⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => _⟩
𝕜 : Type ?u.232896
𝕝 : Type ?u.232899
E : Type u_1
ι : Sort ?u.232905
κ : ι → Sort ?u.232910
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
𝕜 : Type ?u.232896
𝕝 : Type ?u.232899
E : Type u_1
ι : Sort ?u.232905
κ : ι → Sort ?u.232910
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
rw [Real.norm_eq_abs, abs_le] at ha
𝕜 : Type ?u.232896
𝕝 : Type ?u.232899
E : Type u_1
ι : Sort ?u.232905
κ : ι → Sort ?u.232910
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s
𝕜 : Type ?u.232896
𝕝 : Type ?u.232899
E : Type u_1
ι : Sort ?u.232905
κ : ι → Sort ?u.232910
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
rw [show a = -((1 - a) / 2) + (a - -1) / 2 by ring, add_smul, neg_smul, ← smul_neg]
no goals
𝕜 : Type ?u.232896
𝕝 : Type ?u.232899
E : Type u_1
ι : Sort ?u.232905
κ : ι → Sort ?u.232910
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s
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)
no goals
𝕜 : Type ?u.232896
𝕝 : Type ?u.232899
E : Type u_1
ι : Sort ?u.232905
κ : ι → Sort ?u.232910
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a = -((1 - a) / 2) + (a - -1) / 2
ring
no goals
𝕜 : Type ?u.232896
𝕝 : Type ?u.232899
E : Type u_1
ι : Sort ?u.232905
κ : ι → Sort ?u.232910
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ (1 - a) / 2 + (a - -1) / 2 = 1
ring