ι : Sort ?u.37567
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
h : x ∈ s
⊢ infEdist x t ≤ (⨆ (x : α) (_ : x ∈ s), infEdist x t) ⊔ ⨆ (y : α) (_ : y ∈ t), infEdist y s
ι : Sort ?u.37567
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
h : x ∈ s
⊢ infEdist x t ≤ hausdorffEdist s t
rw [hausdorffEdist_def]
ι : Sort ?u.37567
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
h : x ∈ s
⊢ infEdist x t ≤ ⨆ (x : α) (_ : x ∈ s), infEdist x t
ι : Sort ?u.37567
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
h : x ∈ s
⊢ infEdist x t ≤ (⨆ (x : α) (_ : x ∈ s), infEdist x t) ⊔ ⨆ (y : α) (_ : y ∈ t), infEdist y s
refine le_trans ?_ le_sup_left
no goals
ι : Sort ?u.37567
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
h : x ∈ s
⊢ infEdist x t ≤ ⨆ (x : α) (_ : x ∈ s), infEdist x t
exact le_iSup₂ (α := ℝ≥0∞) x h