case mp
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ dist f g < C → ∀ (x : α), dist (↑f x) (↑g x) < C

case mpr
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ (∀ (x : α), dist (↑f x) (↑g x) < C) → dist f g < C
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ dist f g < C ↔ ∀ (x : α), dist (↑f x) (↑g x) < C
fconstructor
case mp
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
w : dist f g < C
x : α
⊢ dist (↑f x) (↑g x) < C
case mp
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ dist f g < C → ∀ (x : α), dist (↑f x) (↑g x) < C
intro w x
no goals
case mp
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
w : dist f g < C
x : α
⊢ dist (↑f x) (↑g x) < C
exact lt_of_le_of_lt (dist_coe_le_dist x) w
case pos
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : Nonempty α
⊢ (∀ (x : α), dist (↑f x) (↑g x) < C) → dist f g < C

case neg
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ (∀ (x : α), dist (↑f x) (↑g x) < C) → dist f g < C
case mpr
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ (∀ (x : α), dist (↑f x) (↑g x) < C) → dist f g < C
by_cases h : Nonempty α
no goals
case pos
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : Nonempty α
⊢ (∀ (x : α), dist (↑f x) (↑g x) < C) → dist f g < C
exact dist_lt_of_nonempty_compact
case neg
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g < C
case neg
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ (∀ (x : α), dist (↑f x) (↑g x) < C) → dist f g < C
rintro -
case h.e'_3
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g = 0
case neg
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g < C
convert C0
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g ≤ 0
case h.e'_3
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g = 0
apply le_antisymm _ dist_nonneg'
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (↑f x) (↑g x) ≤ C} ≤ 0
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g ≤ 0
rw [dist_eq]
no goals
F : Type ?u.285808
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (↑f x) (↑g x) ≤ C} ≤ 0
exact csInf_le ⟨0, fun C => And.left⟩ ⟨le_rfl, fun x => False.elim (h (Nonempty.intro x))⟩