English
If s is strictly convex, then the affine combination x + t(y − x) lies in interior s for 0 < t < 1 when x,y ∈ s.
Русский
Если s строго выпукло, то аффинная комбинация x + t(y − x) находится во внутренности s при 0 < t < 1, когда x,y ∈ s.
LaTeX
$$$\StrictConvex 𝕜 s \rightarrow \forall x,y \in s, x \neq y, \forall t\in(0,1),\; x + t(y-x) \in interior s$$$
Lean4
/-- The preimage of a strictly convex set under an affine map is strictly convex. -/
theorem affine_preimage {s : Set F} (hs : StrictConvex 𝕜 s) {f : E →ᵃ[𝕜] F} (hf : Continuous f) (hfinj : Injective f) :
StrictConvex 𝕜 (f ⁻¹' s) := by
intro x hx y hy hxy a b ha hb hab
refine preimage_interior_subset_interior_preimage hf ?_
rw [mem_preimage, Convex.combo_affine_apply hab]
exact hs hx hy (hfinj.ne hxy) ha hb hab
