case intro.intro.intro.intro
𝕜 : Type u_4
𝕝 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.14448
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
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_4
𝕝 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.14448
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
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
case intro.intro.intro.intro
𝕜 : Type u_4
𝕝 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.14448
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
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
⊢ ↑f (a • x + b • y) = a • ↑f x + b • ↑f y
case intro.intro.intro.intro
𝕜 : Type u_4
𝕝 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.14448
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
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)
refine' hf.image_interior_subset _ ⟨a • x + b • y, hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, _⟩
no goals
case intro.intro.intro.intro
𝕜 : Type u_4
𝕝 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.14448
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
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
⊢ ↑f (a • x + b • y) = a • ↑f x + b • ↑f y
rw [map_add, f.map_smul_of_tower a, f.map_smul_of_tower b]