case refine_1
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
⊢ ∃ t, ∅ ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s))

case refine_2
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
⊢ ∀ ⦃s_1 t : Set β⦄,
    s_1 ⊆ t →
      (∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))) → ∃ t, s_1 ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s))

case refine_3
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
⊢ ∀ ⦃s_1 t : Set β⦄,
    (∃ t, s_1 ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s))) →
      (∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))) →
        ∃ t_1, s_1 ∪ t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))

case refine_4
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
⊢ ∀ (x : β), x ∈ k → ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s))
refine hk.induction_on ?_ ?_ ?_ ?_
no goals
case refine_1
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
⊢ ∃ t, ∅ ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s))
exact ⟨∅, Subset.rfl, isOpen_empty, by simp only [image_empty, bounded_empty, empty_inter]⟩
no goals
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
⊢ Bounded (f '' (∅ ∩ s))
simp only [image_empty, bounded_empty, empty_inter]
case refine_2.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝¹ t✝ : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s✝ : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s✝ x
s s' : Set β
hss' : s ⊆ s'
t : Set β
s't : s' ⊆ t
t_open : IsOpen t
t_bounded : Bounded (f '' (t ∩ s✝))
⊢ ∃ t, s ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s✝))
case refine_2
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
⊢ ∀ ⦃s_1 t : Set β⦄,
    s_1 ⊆ t →
      (∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))) → ∃ t, s_1 ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s))
rintro s s' hss' ⟨t, s't, t_open, t_bounded⟩
no goals
case refine_2.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝¹ t✝ : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s✝ : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s✝ x
s s' : Set β
hss' : s ⊆ s'
t : Set β
s't : s' ⊆ t
t_open : IsOpen t
t_bounded : Bounded (f '' (t ∩ s✝))
⊢ ∃ t, s ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s✝))
exact ⟨t, hss'.trans s't, t_open, t_bounded⟩
case refine_3.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝¹ t✝ : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s✝ : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s✝ x
s s' t : Set β
st : s ⊆ t
t_open : IsOpen t
t_bounded : Bounded (f '' (t ∩ s✝))
t' : Set β
s't' : s' ⊆ t'
t'_open : IsOpen t'
t'_bounded : Bounded (f '' (t' ∩ s✝))
⊢ ∃ t, s ∪ s' ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s✝))
case refine_3
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
⊢ ∀ ⦃s_1 t : Set β⦄,
    (∃ t, s_1 ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s))) →
      (∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))) →
        ∃ t_1, s_1 ∪ t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
rintro s s' ⟨t, st, t_open, t_bounded⟩ ⟨t', s't', t'_open, t'_bounded⟩
case refine_3.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝¹ t✝ : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s✝ : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s✝ x
s s' t : Set β
st : s ⊆ t
t_open : IsOpen t
t_bounded : Bounded (f '' (t ∩ s✝))
t' : Set β
s't' : s' ⊆ t'
t'_open : IsOpen t'
t'_bounded : Bounded (f '' (t' ∩ s✝))
⊢ Bounded (f '' ((t ∪ t') ∩ s✝))
case refine_3.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝¹ t✝ : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s✝ : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s✝ x
s s' t : Set β
st : s ⊆ t
t_open : IsOpen t
t_bounded : Bounded (f '' (t ∩ s✝))
t' : Set β
s't' : s' ⊆ t'
t'_open : IsOpen t'
t'_bounded : Bounded (f '' (t' ∩ s✝))
⊢ ∃ t, s ∪ s' ⊆ t ∧ IsOpen t ∧ Bounded (f '' (t ∩ s✝))
refine' ⟨t ∪ t', union_subset_union st s't', t_open.union t'_open, _⟩
case refine_3.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝¹ t✝ : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s✝ : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s✝ x
s s' t : Set β
st : s ⊆ t
t_open : IsOpen t
t_bounded : Bounded (f '' (t ∩ s✝))
t' : Set β
s't' : s' ⊆ t'
t'_open : IsOpen t'
t'_bounded : Bounded (f '' (t' ∩ s✝))
⊢ Bounded (f '' (t ∩ s✝) ∪ f '' (t' ∩ s✝))
case refine_3.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝¹ t✝ : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s✝ : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s✝ x
s s' t : Set β
st : s ⊆ t
t_open : IsOpen t
t_bounded : Bounded (f '' (t ∩ s✝))
t' : Set β
s't' : s' ⊆ t'
t'_open : IsOpen t'
t'_bounded : Bounded (f '' (t' ∩ s✝))
⊢ Bounded (f '' ((t ∪ t') ∩ s✝))
rw [union_inter_distrib_right, image_union]
no goals
case refine_3.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝¹ t✝ : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s✝ : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s✝ x
s s' t : Set β
st : s ⊆ t
t_open : IsOpen t
t_bounded : Bounded (f '' (t ∩ s✝))
t' : Set β
s't' : s' ⊆ t'
t'_open : IsOpen t'
t'_bounded : Bounded (f '' (t' ∩ s✝))
⊢ Bounded (f '' (t ∩ s✝) ∪ f '' (t' ∩ s✝))
exact t_bounded.union t'_bounded
case refine_4
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
⊢ ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
case refine_4
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
⊢ ∀ (x : β), x ∈ k → ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
intro x hx
case refine_4
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
⊢ ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
case refine_4
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
⊢ ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
have A : ball (f x) 1 ∈ 𝓝 (f x) := ball_mem_nhds _ zero_lt_one
case refine_4
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
⊢ ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
case refine_4
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
⊢ ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
have B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x := hf x hx A
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' ball (f x) 1

case refine_4.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
case refine_4
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
⊢ ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
obtain ⟨u, u_open, xu, uf⟩ : ∃ u : Set β, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' ball (f x) 1
case refine_4.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' ball (f x) 1

case refine_4.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
exact _root_.mem_nhdsWithin.1 B
case refine_4.intro.intro.intro.refine'_1
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ u ∈ 𝓝[k] x

case refine_4.intro.intro.intro.refine'_2
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ Bounded (f '' (u ∩ s))
case refine_4.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ ∃ t, t ∈ 𝓝[k] x ∧ ∃ t_1, t ⊆ t_1 ∧ IsOpen t_1 ∧ Bounded (f '' (t_1 ∩ s))
refine' ⟨u, _, u, Subset.rfl, u_open, _⟩
case refine_4.intro.intro.intro.refine'_1.a
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ u ∈ 𝓝 x
case refine_4.intro.intro.intro.refine'_1
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ u ∈ 𝓝[k] x
apply nhdsWithin_le_nhds
no goals
case refine_4.intro.intro.intro.refine'_1.a
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ u ∈ 𝓝 x
exact u_open.mem_nhds xu
case refine_4.intro.intro.intro.refine'_2
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ Bounded (f '' (f ⁻¹' ball (f x) 1))
case refine_4.intro.intro.intro.refine'_2
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ Bounded (f '' (u ∩ s))
apply Bounded.mono (image_subset _ uf)
no goals
case refine_4.intro.intro.intro.refine'_2
α : Type u
β : Type v
X : Type ?u.522380
ι : Type ?u.522383
inst✝¹ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x
x : β
hx : x ∈ k
A : ball (f x) 1 ∈ 𝓝 (f x)
B : f ⁻¹' ball (f x) 1 ∈ 𝓝[s] x
u : Set β
u_open : IsOpen u
xu : x ∈ u
uf : u ∩ s ⊆ f ⁻¹' ball (f x) 1
⊢ Bounded (f '' (f ⁻¹' ball (f x) 1))
exact bounded_ball.mono (image_preimage_subset _ _)