English
If s is convex and x is in the interior of s, then the closure of s is contained in the interior of the image of the interior of s under a homothety about x with scale t>1.
Русский
Если s выпукло и x ∈ interior(s), то closure(s) ⊆ interior(homothety_x_t'' interior(s)) для t>1.
LaTeX
$$closure s ⊆ interior (homothety x t '' interior 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 closure_subset_interior_image_homothety_of_one_lt {s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s)
(t : ℝ) (ht : 1 < t) : closure s ⊆ interior (homothety x t '' s) :=
(hs.closure_subset_image_homothety_interior_of_one_lt hx t ht).trans <|
(homothety_isOpenMap x t (one_pos.trans ht).ne').image_interior_subset _
