Theorems · Theorem · general topology

eventually_homothety_mem_of_mem_interior

∀ (R : Type u_1) {W : Type u_4} {Q : Type u_5} [inst : AddCommGroup W] [inst_1 : TopologicalSpace W]
  [inst_2 : AddTorsor W Q] [inst_3 : TopologicalSpace Q] [IsTopologicalAddTorsor Q] [inst_5 : CommRing R]
  [inst_6 : TopologicalSpace R] [inst_7 : Module R W] [ContinuousSMul R W] (x : Q) {s : Set Q} {y : Q},
  y ∈ interior s → ∀ᶠ (δ : R) in nhds 1, (AffineMap.homothety x δ) y ∈ s

Defined in

Mathlib.Topology.Algebra.Affine

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupTopologicalSpaceAddTorsorTopologicalSpaceIsTopologicalAddTorsorCommRingTopologicalSpaceModuleContinuousSMul