Theorems · Theorem · convex and discrete geometry

Convex.closure_subset_image_homothety_interior_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 ⊆ ⇑(AffineMap.homothety x t) '' interior s

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.

Defined in

Mathlib.Analysis.Convex.Topology

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul