case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.205460
E : Type u_2
F : Type u_3
β : Type ?u.205469
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ : E
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : IsOpenMap ↑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : ↑f x ≠ ↑f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • ↑f x + b • ↑f y ∈ interior (↑f '' s)
𝕜 : Type u_1
𝕝 : Type ?u.205460
E : Type u_2
F : Type u_3
β : Type ?u.205469
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : IsOpenMap ↑f
⊢ StrictConvex 𝕜 (↑f '' s)
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab
no goals
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.205460
E : Type u_2
F : Type u_3
β : Type ?u.205469
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ : E
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : IsOpenMap ↑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : ↑f x ≠ ↑f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • ↑f x + b • ↑f y ∈ interior (↑f '' s)
exact
  hf.image_interior_subset _
    ⟨a • x + b • y, ⟨hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, Convex.combo_affine_apply hab⟩⟩