case intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
⊢ ∃ y, y ∈ s ∧ infDist x s = dist x y
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
hne : Set.Nonempty s
x : α
⊢ ∃ y, y ∈ s ∧ infDist x s = dist x y
rcases hne with ⟨z, hz⟩
case intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
⊢ ∃ y, y ∈ s ∧ infDist x (s ∩ closedBall x (dist z x)) = dist x y
case intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
⊢ ∃ y, y ∈ s ∧ infDist x s = dist x y
rw [← infDist_inter_closedBall_of_mem hz]
case intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
case intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
⊢ ∃ y, y ∈ s ∧ infDist x (s ∩ closedBall x (dist z x)) = dist x y
set t := s ∩ closedBall x (dist z x)
case intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
case intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
have htc : IsCompact t := (isCompact_closedBall x (dist z x)).inter_left h
case intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : Set.Nonempty t
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
case intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
have htne : t.Nonempty := ⟨z, hz, mem_closedBall.2 le_rfl⟩
case intro.intro.intro.intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y✝ : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : Set.Nonempty t
y : α
hyd : infDist x t = dist x y
hys : y ∈ s
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
case intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : Set.Nonempty t
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
obtain ⟨y, ⟨hys, -⟩, hyd⟩ : ∃ y ∈ t, infDist x t = dist x y := htc.exists_infDist_eq_dist htne x
no goals
case intro.intro.intro.intro
ι : Sort ?u.69127
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y✝ : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : Set.Nonempty t
y : α
hyd : infDist x t = dist x y
hys : y ∈ s
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
exact ⟨y, hys, hyd⟩