F : Type ?u.276668
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (↑f x) (↑g x) < C
c : Continuous fun x => dist (↑f x) (↑g x)
⊢ dist f g < C
F : Type ?u.276668
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (↑f x) (↑g x) < C
⊢ dist f g < C
have c : Continuous fun x => dist (f x) (g x) := by continuity
case intro.intro
F : Type ?u.276668
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (↑f x) (↑g x) < C
c : Continuous fun x => dist (↑f x) (↑g x)
x : α
le : IsMaxOn (fun x => dist (↑f x) (↑g x)) univ x
⊢ dist f g < C
F : Type ?u.276668
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (↑f x) (↑g x) < C
c : Continuous fun x => dist (↑f x) (↑g x)
⊢ dist f g < C
obtain ⟨x, -, le⟩ :=
  IsCompact.exists_isMaxOn isCompact_univ Set.univ_nonempty (Continuous.continuousOn c)
no goals
case intro.intro
F : Type ?u.276668
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (↑f x) (↑g x) < C
c : Continuous fun x => dist (↑f x) (↑g x)
x : α
le : IsMaxOn (fun x => dist (↑f x) (↑g x)) univ x
⊢ dist f g < C
exact lt_of_le_of_lt (dist_le_iff_of_nonempty.mpr fun y => le trivial) (w x)
no goals
F : Type ?u.276668
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (↑f x) (↑g x) < C
⊢ Continuous fun x => dist (↑f x) (↑g x)
continuity