subset_interior_image_homothety_of_one_lt

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

Похожие утверждения