ι : Sort ?u.35968
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → infEdist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infEdist x s ≤ r
⊢ (∀ (i : α), i ∈ s → infEdist i t ≤ r) ∧ ∀ (i : α), i ∈ t → infEdist i s ≤ r
ι : Sort ?u.35968
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → infEdist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infEdist x s ≤ r
⊢ hausdorffEdist s t ≤ r
simp only [hausdorffEdist_def, sup_le_iff, iSup_le_iff]
no goals
ι : Sort ?u.35968
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → infEdist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infEdist x s ≤ r
⊢ (∀ (i : α), i ∈ s → infEdist i t ≤ r) ∧ ∀ (i : α), i ∈ t → infEdist i s ≤ r
exact ⟨H1, H2⟩