Theorems · Theorem · convex and discrete geometry

Convex.closure_subset_interior_image_homothety_of_one_lt

∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] {s : Set E},
  Convex ℝ s → ∀ {x : E}, x ∈ interior s → ∀ (t : ℝ), 1 < t → closure s ⊆ interior (⇑(AffineMap.homothety x t) '' s)

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.

Defined in

Mathlib.Analysis.Convex.Topology

Cited by

1 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul