α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
⊢ IsCompact (closedBall x₀ r)
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont : Continuous f
hf : Function.Surjective f
⊢ ProperSpace β
refine ⟨fun x₀ r => ?_⟩
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
⊢ IsCompact (closedBall x₀ r)
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
⊢ IsCompact (closedBall x₀ r)
let K := f ⁻¹' closedBall x₀ r
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
⊢ IsCompact (closedBall x₀ r)
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
⊢ IsCompact (closedBall x₀ r)
have A : IsClosed K := isClosed_ball.preimage f_cont
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
⊢ IsCompact (closedBall x₀ r)
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
⊢ IsCompact (closedBall x₀ r)
have B : Bounded K := hK.bounded_preimage bounded_closedBall
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
this : IsCompact K
⊢ IsCompact (closedBall x₀ r)
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
⊢ IsCompact (closedBall x₀ r)
have : IsCompact K := isCompact_iff_isClosed_bounded.2 ⟨A, B⟩
case h.e'_3
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
this : IsCompact K
⊢ closedBall x₀ r = f '' K
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
this : IsCompact K
⊢ IsCompact (closedBall x₀ r)
convert this.image f_cont
no goals
case h.e'_3
α✝ : Type ?u.96684
β : Type u_2
γ : Type ?u.96690
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_1
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
this : IsCompact K
⊢ closedBall x₀ r = f '' K
exact (hf.image_preimage _).symm