case inl
F : Type ?u.306605
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
h✝ : IsEmpty α
⊢ dist f g = ⨆ (x : α), dist (↑f x) (↑g x)

case inr
F : Type ?u.306605
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
h✝ : Nonempty α
⊢ dist f g = ⨆ (x : α), dist (↑f x) (↑g x)
F : Type ?u.306605
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ dist f g = ⨆ (x : α), dist (↑f x) (↑g x)
cases isEmpty_or_nonempty α
case inr
F : Type ?u.306605
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
h✝ : Nonempty α
⊢ BddAbove (range fun x => dist (↑f x) (↑g x))
case inr
F : Type ?u.306605
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
h✝ : Nonempty α
⊢ dist f g = ⨆ (x : α), dist (↑f x) (↑g x)
refine' (dist_le_iff_of_nonempty.mpr <| le_ciSup _).antisymm (ciSup_le dist_coe_le_dist)
no goals
case inr
F : Type ?u.306605
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
h✝ : Nonempty α
⊢ BddAbove (range fun x => dist (↑f x) (↑g x))
exact dist_set_exists.imp fun C hC => forall_range_iff.2 hC.2
no goals
case inl
F : Type ?u.306605
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
h✝ : IsEmpty α
⊢ dist f g = ⨆ (x : α), dist (↑f x) (↑g x)
rw [iSup_of_empty', Real.sSup_empty, dist_zero_of_empty]