English
If s is convex and x lies in the interior of s, then s is contained in the interior of the image of s under the homothety with centre x and factor t>1.
Русский
Если s выпукло и x ∈ interior(s), то s ⊆ interior(homothety_x t '' s).
LaTeX
$$s ⊆ interior (homothety x t '' s), \; t>1$$
Lean4
/-- If we dilate a convex set about a point in its interior by a scale `t > 1`, the interior of
the result includes the closure of the original set.
TODO Generalise this from convex sets to sets that are balanced / star-shaped about `x`. -/
theorem subset_interior_image_homothety_of_one_lt {s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ)
(ht : 1 < t) : s ⊆ interior (homothety x t '' s) :=
subset_closure.trans <| hs.closure_subset_interior_image_homothety_of_one_lt hx t ht