English
If s is convex and x is in the interior of s, then the closure of s is contained in the image of the interior of s under a homothety about x with scale t>1.
Русский
Если s выпукло и точка x принадлежитInterior(s), то замыкание s содержится в образеInterior(s) под гомотетией вокруг x с масштабом t>1.
LaTeX
$$closure s ⊆ homothety x t '' interior s, \; t>1, \; x ∈ interior s$$
Lean4
/-- If we dilate the interior of a convex set about a point in its interior by a scale `t > 1`,
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_image_homothety_interior_of_one_lt {s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s)
(t : ℝ) (ht : 1 < t) : closure s ⊆ homothety x t '' interior s :=
by
intro y hy
have hne : t ≠ 0 := (one_pos.trans ht).ne'
refine
⟨homothety x t⁻¹ y, hs.openSegment_interior_closure_subset_interior hx hy ?_,
(AffineEquiv.homothetyUnitsMulHom x (Units.mk0 t hne)).apply_symm_apply y⟩
rw [openSegment_eq_image_lineMap, ← inv_one, ← inv_Ioi₀ (zero_lt_one' ℝ), ← image_inv_eq_inv, image_image,
homothety_eq_lineMap]
exact mem_image_of_mem _ ht
