𝕜 : Type u_1
𝕝 : Type ?u.221625
E : Type u_2
F : Type ?u.221631
β : Type ?u.221634
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ a / (a + b) + b / (a + b) = 1
𝕜 : Type u_1
𝕝 : Type ?u.221625
E : Type u_2
F : Type ?u.221631
β : Type ?u.221634
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
apply h hx hy hxy (div_pos ha <| add_pos ha hb) (div_pos hb <| add_pos ha hb)
𝕜 : Type u_1
𝕝 : Type ?u.221625
E : Type u_2
F : Type ?u.221631
β : Type ?u.221634
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ (a + b) / (a + b) = 1
𝕜 : Type u_1
𝕝 : Type ?u.221625
E : Type u_2
F : Type ?u.221631
β : Type ?u.221634
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ a / (a + b) + b / (a + b) = 1
rw [← add_div]
no goals
𝕜 : Type u_1
𝕝 : Type ?u.221625
E : Type u_2
F : Type ?u.221631
β : Type ?u.221634
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ (a + b) / (a + b) = 1
exact div_self (add_pos ha hb).ne'
no goals
𝕜 : Type u_1
𝕝 : Type ?u.221625
E : Type u_2
F : Type ?u.221631
β : Type ?u.221634
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s
convert h hx hy hxy ha hb <;> rw [hab, div_one]