𝕜 : Type u_1
𝕝 : Type ?u.66499
E : Type u_2
F : Type ?u.66505
β : Type ?u.66508
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior ((fun x => z + x) ⁻¹' s)
𝕜 : Type u_1
𝕝 : Type ?u.66499
E : Type u_2
F : Type ?u.66505
β : Type ?u.66508
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x => z + x) ⁻¹' s)
intro x hx y hy hxy a b ha hb hab
𝕜 : Type u_1
𝕝 : Type ?u.66499
E : Type u_2
F : Type ?u.66505
β : Type ?u.66508
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s
𝕜 : Type u_1
𝕝 : Type ?u.66499
E : Type u_2
F : Type ?u.66505
β : Type ?u.66508
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior ((fun x => z + x) ⁻¹' s)
refine' preimage_interior_subset_interior_preimage (continuous_add_left _) _
𝕜 : Type u_1
𝕝 : Type ?u.66499
E : Type u_2
F : Type ?u.66505
β : Type ?u.66508
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : a • (fun x => z + x) x + b • (fun x => z + x) y ∈ interior s
⊢ a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s
𝕜 : Type u_1
𝕝 : Type ?u.66499
E : Type u_2
F : Type ?u.66505
β : Type ?u.66508
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s
have h := hs hx hy ((add_right_injective _).ne hxy) ha hb hab
no goals
𝕜 : Type u_1
𝕝 : Type ?u.66499
E : Type u_2
F : Type ?u.66505
β : Type ?u.66508
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : a • (fun x => z + x) x + b • (fun x => z + x) y ∈ interior s
⊢ a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s
rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h