case pos
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : hausdorffEdist s t = ⊤
⊢ hausdorffDist s t ≤ r

case neg
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
⊢ hausdorffDist s t ≤ r
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
⊢ hausdorffDist s t ≤ r
by_cases h1 : hausdorffEdist s t = ⊤
case neg.inl
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : s = ∅
⊢ hausdorffDist s t ≤ r

case neg.inr
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
⊢ hausdorffDist s t ≤ r
case neg
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
⊢ hausdorffDist s t ≤ r
cases' s.eq_empty_or_nonempty with hs hs
case neg.inr.inl
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : t = ∅
⊢ hausdorffDist s t ≤ r

case neg.inr.inr
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ hausdorffDist s t ≤ r
case neg.inr
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
⊢ hausdorffDist s t ≤ r
cases' t.eq_empty_or_nonempty with ht ht
no goals
case neg.inr.inr
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
this : hausdorffEdist s t ≤ ENNReal.ofReal r
⊢ hausdorffDist s t ≤ r
rwa [hausdorffDist, ← ENNReal.toReal_ofReal hr,
  ENNReal.toReal_le_toReal h1 ENNReal.ofReal_ne_top]
no goals
case pos
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : hausdorffEdist s t = ⊤
⊢ hausdorffDist s t ≤ r
rwa [hausdorffDist, h1, ENNReal.top_toReal]
no goals
case neg.inl
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : s = ∅
⊢ hausdorffDist s t ≤ r
rwa [hs, hausdorffDist_empty']
no goals
case neg.inr.inl
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : t = ∅
⊢ hausdorffDist s t ≤ r
rwa [ht, hausdorffDist_empty]
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ ∀ (x : α), x ∈ s → infEdist x t ≤ ENNReal.ofReal r

ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ ∀ (x : α), x ∈ t → infEdist x s ≤ ENNReal.ofReal r
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ hausdorffEdist s t ≤ ENNReal.ofReal r
apply hausdorffEdist_le_of_infEdist _ _
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ s
⊢ infEdist x t ≤ ENNReal.ofReal r
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ ∀ (x : α), x ∈ s → infEdist x t ≤ ENNReal.ofReal r
intro x hx
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ s
I : infDist x t ≤ r
⊢ infEdist x t ≤ ENNReal.ofReal r
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ s
⊢ infEdist x t ≤ ENNReal.ofReal r
have I := H1 x hx
no goals
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ s
I : infDist x t ≤ r
⊢ infEdist x t ≤ ENNReal.ofReal r
rwa [infDist, ← ENNReal.toReal_ofReal hr,
  ENNReal.toReal_le_toReal (infEdist_ne_top ht) ENNReal.ofReal_ne_top] at I
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ t
⊢ infEdist x s ≤ ENNReal.ofReal r
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ ∀ (x : α), x ∈ t → infEdist x s ≤ ENNReal.ofReal r
intro x hx
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ t
I : infDist x s ≤ r
⊢ infEdist x s ≤ ENNReal.ofReal r
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ t
⊢ infEdist x s ≤ ENNReal.ofReal r
have I := H2 x hx
no goals
ι : Sort ?u.75570
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ t
I : infDist x s ≤ r
⊢ infEdist x s ≤ ENNReal.ofReal r
rwa [infDist, ← ENNReal.toReal_ofReal hr,
  ENNReal.toReal_le_toReal (infEdist_ne_top hs) ENNReal.ofReal_ne_top] at I