α : Type ?u.95109
V : Type ?u.95112
P : Type ?u.95115
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
⊢ ∀ (y : Q), y ∈ t → ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
α : Type ?u.95109
V : Type ?u.95112
P : Type ?u.95115
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) '' t ⊆ s
suffices ∀ y ∈ t, ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s by
  simp_rw [Set.image_subset_iff]
  exact (Filter.eventually_all_finite ht).mpr this
α : Type ?u.95109
V : Type ?u.95112
P : Type ?u.95115
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
y : Q
hy : y ∈ t
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
α : Type ?u.95109
V : Type ?u.95112
P : Type ?u.95115
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
⊢ ∀ (y : Q), y ∈ t → ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
intro y hy
no goals
α : Type ?u.95109
V : Type ?u.95112
P : Type ?u.95115
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
y : Q
hy : y ∈ t
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
exact eventually_homothety_mem_of_mem_interior 𝕜 x (h hy)
α : Type ?u.95109
V : Type ?u.95112
P : Type ?u.95115
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
this : ∀ (y : Q), y ∈ t → ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, t ⊆ (fun a => ↑(homothety x δ) a) ⁻¹' s
α : Type ?u.95109
V : Type ?u.95112
P : Type ?u.95115
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
this : ∀ (y : Q), y ∈ t → ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) '' t ⊆ s
simp_rw [Set.image_subset_iff]
no goals
α : Type ?u.95109
V : Type ?u.95112
P : Type ?u.95115
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
this : ∀ (y : Q), y ∈ t → ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, t ⊆ (fun a => ↑(homothety x δ) a) ⁻¹' s
exact (Filter.eventually_all_finite ht).mpr this