ι : Sort ?u.27190
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
hs : IsCompact s
hne : Set.Nonempty s
x : α
A : Continuous fun y => edist x y
⊢ ∃ y, y ∈ s ∧ infEdist x s = edist x y
ι : Sort ?u.27190
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
hs : IsCompact s
hne : Set.Nonempty s
x : α
⊢ ∃ y, y ∈ s ∧ infEdist x s = edist x y
have A : Continuous fun y => edist x y := continuous_const.edist continuous_id
case intro.intro
ι : Sort ?u.27190
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t : Set α
Φ : α → β
hs : IsCompact s
hne : Set.Nonempty s
x : α
A : Continuous fun y => edist x y
y : α
ys : y ∈ s
hy : ∀ (z : α), z ∈ s → edist x y ≤ edist x z
⊢ ∃ y, y ∈ s ∧ infEdist x s = edist x y
ι : Sort ?u.27190
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
hs : IsCompact s
hne : Set.Nonempty s
x : α
A : Continuous fun y => edist x y
⊢ ∃ y, y ∈ s ∧ infEdist x s = edist x y
obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, ∀ z, z ∈ s → edist x y ≤ edist x z :=
  hs.exists_forall_le hne A.continuousOn
no goals
case intro.intro
ι : Sort ?u.27190
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t : Set α
Φ : α → β
hs : IsCompact s
hne : Set.Nonempty s
x : α
A : Continuous fun y => edist x y
y : α
ys : y ∈ s
hy : ∀ (z : α), z ∈ s → edist x y ≤ edist x z
⊢ ∃ y, y ∈ s ∧ infEdist x s = edist x y
exact ⟨y, ys, le_antisymm (infEdist_le_edist_of_mem ys) (by rwa [le_infEdist])⟩
no goals
ι : Sort ?u.27190
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t : Set α
Φ : α → β
hs : IsCompact s
hne : Set.Nonempty s
x : α
A : Continuous fun y => edist x y
y : α
ys : y ∈ s
hy : ∀ (z : α), z ∈ s → edist x y ≤ edist x z
⊢ edist x y ≤ infEdist x s
rwa [le_infEdist]