[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g✝ : α →ᵇ β
x : α
C : ℝ
g : α →ᵇ β
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
map_bounded'✝ :
  ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk toFun✝) x) (ContinuousMap.toFun (ContinuousMap.mk toFun✝) y) ≤ C
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, map_bounded' := map_bounded'✝ } =
    (fun f => f.toFun) g
⊢ { toContinuousMap := ContinuousMap.mk toFun✝, map_bounded' := map_bounded'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
map_bounded'✝¹ :
  ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk toFun✝¹) x) (ContinuousMap.toFun (ContinuousMap.mk toFun✝¹) y) ≤ C
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
map_bounded'✝ :
  ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk toFun✝) x) (ContinuousMap.toFun (ContinuousMap.mk toFun✝) y) ≤ C
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝¹, map_bounded' := map_bounded'✝¹ } =
    (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, map_bounded' := map_bounded'✝ }
⊢ { toContinuousMap := ContinuousMap.mk toFun✝¹, map_bounded' := map_bounded'✝¹ } =
    { toContinuousMap := ContinuousMap.mk toFun✝, map_bounded' := map_bounded'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : α), dist (↑f x) (↑g x) ≤ C
[PROOFSTEP]
rcases f.bounded_range.union g.bounded_range with ⟨C, hC⟩
[GOAL]
case intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C✝ C : ℝ
hC : ∀ (x : β), x ∈ range ↑f ∪ range ↑g → ∀ (y : β), y ∈ range ↑f ∪ range ↑g → dist x y ≤ C
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : α), dist (↑f x) (↑g x) ≤ C
[PROOFSTEP]
refine' ⟨max 0 C, le_max_left _ _, fun x => (hC _ _ _ _).trans (le_max_right _ _)⟩ <;> [left; right]
[GOAL]
case intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C✝ C : ℝ
hC : ∀ (x : β), x ∈ range ↑f ∪ range ↑g → ∀ (y : β), y ∈ range ↑f ∪ range ↑g → dist x y ≤ C
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : α), dist (↑f x) (↑g x) ≤ C
[PROOFSTEP]
refine' ⟨max 0 C, le_max_left _ _, fun x => (hC _ _ _ _).trans (le_max_right _ _)⟩
[GOAL]
case intro.refine'_1
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C✝ C : ℝ
hC : ∀ (x : β), x ∈ range ↑f ∪ range ↑g → ∀ (y : β), y ∈ range ↑f ∪ range ↑g → dist x y ≤ C
x : α
⊢ ↑f x ∈ range ↑f ∪ range ↑g
[PROOFSTEP]
left
[GOAL]
case intro.refine'_2
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C✝ C : ℝ
hC : ∀ (x : β), x ∈ range ↑f ∪ range ↑g → ∀ (y : β), y ∈ range ↑f ∪ range ↑g → dist x y ≤ C
x : α
⊢ ↑g x ∈ range ↑f ∪ range ↑g
[PROOFSTEP]
right
[GOAL]
case intro.refine'_1.h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C✝ C : ℝ
hC : ∀ (x : β), x ∈ range ↑f ∪ range ↑g → ∀ (y : β), y ∈ range ↑f ∪ range ↑g → dist x y ≤ C
x : α
⊢ ↑f x ∈ range ↑f
[PROOFSTEP]
apply mem_range_self
[GOAL]
case intro.refine'_2.h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C✝ C : ℝ
hC : ∀ (x : β), x ∈ range ↑f ∪ range ↑g → ∀ (y : β), y ∈ range ↑f ∪ range ↑g → dist x y ≤ C
x : α
⊢ ↑g x ∈ range ↑g
[PROOFSTEP]
apply mem_range_self
[GOAL]
F : Type u_1
α : 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
[PROOFSTEP]
have c : Continuous fun x => dist (f x) (g x) := by continuity
[GOAL]
F : Type u_1
α : 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)
[PROOFSTEP]
continuity
[GOAL]
F : Type u_1
α : 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
[PROOFSTEP]
obtain ⟨x, -, le⟩ := IsCompact.exists_isMaxOn isCompact_univ Set.univ_nonempty (Continuous.continuousOn c)
[GOAL]
case intro.intro
F : Type u_1
α : 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
[PROOFSTEP]
exact lt_of_le_of_lt (dist_le_iff_of_nonempty.mpr fun y => le trivial) (w x)
[GOAL]
F : Type u_1
α : 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
[PROOFSTEP]
fconstructor
[GOAL]
case mp
F : Type u_1
α : 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
[PROOFSTEP]
intro w x
[GOAL]
case mp
F : Type u_1
α : 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
[PROOFSTEP]
exact lt_of_le_of_lt (dist_coe_le_dist x) w
[GOAL]
case mpr
F : Type u_1
α : 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
[PROOFSTEP]
by_cases h : Nonempty α
[GOAL]
case pos
F : Type u_1
α : 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
[PROOFSTEP]
exact dist_lt_of_nonempty_compact
[GOAL]
case neg
F : Type u_1
α : 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
[PROOFSTEP]
rintro -
[GOAL]
case neg
F : Type u_1
α : 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
[PROOFSTEP]
convert C0
[GOAL]
case h.e'_3
F : Type u_1
α : 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
[PROOFSTEP]
apply le_antisymm _ dist_nonneg'
[GOAL]
F : Type u_1
α : 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
[PROOFSTEP]
rw [dist_eq]
[GOAL]
F : Type u_1
α : 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
[PROOFSTEP]
exact csInf_le ⟨0, fun C => And.left⟩ ⟨le_rfl, fun x => False.elim (h (Nonempty.intro x))⟩
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
f : α →ᵇ β
x : α
⊢ dist (↑f x) (↑f x) ≤ 0
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
⊢ dist f g = dist g f
[PROOFSTEP]
simp [dist_eq, dist_comm]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
x y : α →ᵇ β
⊢ (fun x y => ↑{ val := dist x y, property := (_ : 0 ≤ dist x y) }) x y = ENNReal.ofReal (dist x y)
[PROOFSTEP]
dsimp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
x y : α →ᵇ β
⊢ ↑{ val := dist x y, property := (_ : 0 ≤ dist x y) } = ENNReal.ofReal (dist x y)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_val
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
x y : α →ᵇ β
⊢ dist x y = max (dist x y) 0
[PROOFSTEP]
simp [dist_nonneg']
[GOAL]
F : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : PseudoMetricSpace β✝
inst✝² : PseudoMetricSpace γ
f g : α✝ →ᵇ β✝
x : α✝
C : ℝ
α : Type ?u.332963
β : Type ?u.332966
inst✝¹ : TopologicalSpace α
inst✝ : MetricSpace β
x✝ y✝ : α →ᵇ β
hfg : dist x✝ y✝ = 0
⊢ x✝ = y✝
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : PseudoMetricSpace β✝
inst✝² : PseudoMetricSpace γ
f g : α✝ →ᵇ β✝
x✝¹ : α✝
C : ℝ
α : Type ?u.332963
β : Type ?u.332966
inst✝¹ : TopologicalSpace α
inst✝ : MetricSpace β
x✝ y✝ : α →ᵇ β
hfg : dist x✝ y✝ = 0
x : α
⊢ ↑x✝ x = ↑y✝ x
[PROOFSTEP]
exact eq_of_dist_eq_zero (le_antisymm (hfg ▸ dist_coe_le_dist _) dist_nonneg)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (↑f x) (↑g x) ≤ C} = ↑(sInf {C | ∀ (x : α), nndist (↑f x) (↑g x) ≤ C})
[PROOFSTEP]
rw [val_eq_coe, coe_sInf, coe_image]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (↑f x) (↑g x) ≤ C} =
    sInf {x | ∃ h, { val := x, property := h } ∈ {C | ∀ (x : α), nndist (↑f x) (↑g x) ≤ C}}
[PROOFSTEP]
simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, coe_mk, exists_prop, coe_nndist]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : IsEmpty α
⊢ dist f g = 0
[PROOFSTEP]
rw [(ext isEmptyElim : f = g), dist_self]
[GOAL]
F : Type u_1
α : 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)
[PROOFSTEP]
cases isEmpty_or_nonempty α
[GOAL]
case inl
F : Type u_1
α : 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)
[PROOFSTEP]
rw [iSup_of_empty', Real.sSup_empty, dist_zero_of_empty]
[GOAL]
case inr
F : Type u_1
α : 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)
[PROOFSTEP]
refine' (dist_le_iff_of_nonempty.mpr <| le_ciSup _).antisymm (ciSup_le dist_coe_le_dist)
[GOAL]
case inr
F : Type u_1
α : 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))
[PROOFSTEP]
exact dist_set_exists.imp fun C hC => forall_range_iff.2 hC.2
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ ⨆ (x : α), dist (↑f x) (↑g x) = ↑(⨆ (x : α), nndist (↑f x) (↑g x))
[PROOFSTEP]
simp_rw [val_eq_coe, coe_iSup, coe_nndist]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ Inducing (↑UniformFun.ofFun ∘ FunLike.coe)
[PROOFSTEP]
rw [inducing_iff_nhds]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ ∀ (a : α →ᵇ β), 𝓝 a = comap (↑UniformFun.ofFun ∘ FunLike.coe) (𝓝 ((↑UniformFun.ofFun ∘ FunLike.coe) a))
[PROOFSTEP]
refine' fun f => eq_of_forall_le_iff fun l => _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ l ≤ 𝓝 f ↔ l ≤ comap (↑UniformFun.ofFun ∘ FunLike.coe) (𝓝 ((↑UniformFun.ofFun ∘ FunLike.coe) f))
[PROOFSTEP]
rw [← tendsto_iff_comap, ← tendsto_id', tendsto_iff_tendstoUniformly, UniformFun.tendsto_iff_tendstoUniformly]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ TendstoUniformly (fun i => ↑(id i)) (↑f) l ↔
    TendstoUniformly (↑UniformFun.ofFun ∘ FunLike.coe) ((↑UniformFun.ofFun ∘ FunLike.coe) f) l
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
b : β
⊢ ∀ (x y : α),
    dist (ContinuousMap.toFun (ContinuousMap.const α b) x) (ContinuousMap.toFun (ContinuousMap.const α b) y) ≤ 0
[PROOFSTEP]
simp [le_rfl]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
⊢ ∃ a, Tendsto f atTop (𝓝 a)
[PROOFSTEP]
rcases cauchySeq_iff_le_tendsto_0.1 hf with ⟨b, b0, b_bound, b_lim⟩
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
⊢ ∃ a, Tendsto f atTop (𝓝 a)
[PROOFSTEP]
have f_bdd := fun x n m N hn hm => le_trans (dist_coe_le_dist x) (b_bound n m N hn hm)
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
⊢ ∃ a, Tendsto f atTop (𝓝 a)
[PROOFSTEP]
have fx_cau : ∀ x, CauchySeq fun n => f n x := fun x => cauchySeq_iff_le_tendsto_0.2 ⟨b, b0, f_bdd x, b_lim⟩
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
⊢ ∃ a, Tendsto f atTop (𝓝 a)
[PROOFSTEP]
choose F hF using fun x =>
  cauchySeq_tendsto_of_complete
    (fx_cau x)
      /- `F : α → β`, `hF : ∀ (x : α), Tendsto (fun n ↦ ↑(f n) x) atTop (𝓝 (F x))`
            `F` is the desired limit function. Check that it is uniformly approximated by `f N`. -/
[GOAL]
case intro.intro.intro
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
⊢ ∃ a, Tendsto f atTop (𝓝 a)
[PROOFSTEP]
have fF_bdd : ∀ x N, dist (f N x) (F x) ≤ b N := fun x N =>
  le_of_tendsto (tendsto_const_nhds.dist (hF x))
    (Filter.eventually_atTop.2 ⟨N, fun n hn => f_bdd x N n N (le_refl N) hn⟩)
[GOAL]
case intro.intro.intro
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
⊢ ∃ a, Tendsto f atTop (𝓝 a)
[PROOFSTEP]
refine' ⟨⟨⟨F, _⟩, _⟩, _⟩
[GOAL]
case intro.intro.intro.refine'_1
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
⊢ Continuous F
[PROOFSTEP]
have : TendstoUniformly (fun n x => f n x) F atTop :=
  by
  refine' Metric.tendstoUniformly_iff.2 fun ε ε0 => _
  refine' ((tendsto_order.1 b_lim).2 ε ε0).mono fun n hn x => _
  rw [dist_comm]
  exact lt_of_le_of_lt (fF_bdd x n) hn
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
⊢ TendstoUniformly (fun n x => ↑(f n) x) F atTop
[PROOFSTEP]
refine' Metric.tendstoUniformly_iff.2 fun ε ε0 => _
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), dist (F x) (↑(f n) x) < ε
[PROOFSTEP]
refine' ((tendsto_order.1 b_lim).2 ε ε0).mono fun n hn x => _
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
ε : ℝ
ε0 : ε > 0
n : ℕ
hn : b n < ε
x : α
⊢ dist (F x) (↑(f n) x) < ε
[PROOFSTEP]
rw [dist_comm]
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
ε : ℝ
ε0 : ε > 0
n : ℕ
hn : b n < ε
x : α
⊢ dist (↑(f n) x) (F x) < ε
[PROOFSTEP]
exact lt_of_le_of_lt (fF_bdd x n) hn
[GOAL]
case intro.intro.intro.refine'_1
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
this : TendstoUniformly (fun n x => ↑(f n) x) F atTop
⊢ Continuous F
[PROOFSTEP]
exact this.continuous (eventually_of_forall fun N => (f N).continuous)
[GOAL]
case intro.intro.intro.refine'_2
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
⊢ ∃ C, ∀ (x y : α), dist (ContinuousMap.toFun (ContinuousMap.mk F) x) (ContinuousMap.toFun (ContinuousMap.mk F) y) ≤ C
[PROOFSTEP]
rcases(f 0).bounded with ⟨C, hC⟩
[GOAL]
case intro.intro.intro.refine'_2.intro
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C✝ : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
C : ℝ
hC : ∀ (x y : α), dist (↑(f 0) x) (↑(f 0) y) ≤ C
⊢ ∃ C, ∀ (x y : α), dist (ContinuousMap.toFun (ContinuousMap.mk F) x) (ContinuousMap.toFun (ContinuousMap.mk F) y) ≤ C
[PROOFSTEP]
refine' ⟨C + (b 0 + b 0), fun x y => _⟩
[GOAL]
case intro.intro.intro.refine'_2.intro
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C✝ : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
C : ℝ
hC : ∀ (x y : α), dist (↑(f 0) x) (↑(f 0) y) ≤ C
x y : α
⊢ dist (ContinuousMap.toFun (ContinuousMap.mk F) x) (ContinuousMap.toFun (ContinuousMap.mk F) y) ≤ C + (b 0 + b 0)
[PROOFSTEP]
calc
  dist (F x) (F y) ≤ dist (f 0 x) (f 0 y) + (dist (f 0 x) (F x) + dist (f 0 y) (F y)) := dist_triangle4_left _ _ _ _
  _ ≤ C + (b 0 + b 0) :=
    add_le_add (hC _ _)
      (add_le_add (fF_bdd _ _) (fF_bdd _ _))
        -- porting note: was --by mono*
[GOAL]
case intro.intro.intro.refine'_3
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
⊢ Tendsto f atTop
    (𝓝
      { toContinuousMap := ContinuousMap.mk F,
        map_bounded' :=
          (_ :
            ∃ C,
              ∀ (x y : α),
                dist (ContinuousMap.toFun (ContinuousMap.mk F) x) (ContinuousMap.toFun (ContinuousMap.mk F) y) ≤ C) })
[PROOFSTEP]
refine' tendsto_iff_dist_tendsto_zero.2 (squeeze_zero (fun _ => dist_nonneg) _ b_lim)
[GOAL]
case intro.intro.intro.refine'_3
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist (↑(f n) x) (↑(f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n => ↑(f n) x
F : (x : α) → (fun a => β) x
hF : ∀ (x : α), Tendsto (fun n => ↑(f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist (↑(f N) x) (F x) ≤ b N
⊢ ∀ (t : ℕ),
    dist (f t)
        { toContinuousMap := ContinuousMap.mk F,
          map_bounded' :=
            (_ :
              ∃ C,
                ∀ (x y : α),
                  dist (ContinuousMap.toFun (ContinuousMap.mk F) x) (ContinuousMap.toFun (ContinuousMap.mk F) y) ≤
                    C) } ≤
      b t
[PROOFSTEP]
exact fun N => (dist_le (b0 _)).2 fun x => fF_bdd x N
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C✝ : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f : α →ᵇ β
D : ℝ
hD : ∀ (x y : α), dist (↑f x) (↑f y) ≤ D
x y : α
⊢ ↑C * dist (↑f x) (↑f y) ≤ ↑(max C 0) * dist (↑f x) (↑f y)
[PROOFSTEP]
gcongr
[GOAL]
case h.h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C✝ : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f : α →ᵇ β
D : ℝ
hD : ∀ (x y : α), dist (↑f x) (↑f y) ≤ D
x y : α
⊢ C ≤ max C 0
[PROOFSTEP]
apply le_max_left
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C✝ : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f : α →ᵇ β
D : ℝ
hD : ∀ (x y : α), dist (↑f x) (↑f y) ≤ D
x y : α
⊢ ↑(max C 0) * dist (↑f x) (↑f y) ≤ ↑(max C 0) * D
[PROOFSTEP]
gcongr
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C✝ : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f : α →ᵇ β
D : ℝ
hD : ∀ (x y : α), dist (↑f x) (↑f y) ≤ D
x y : α
⊢ dist (↑f x) (↑f y) ≤ D
[PROOFSTEP]
apply hD
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g✝ : α →ᵇ β
x✝ : α
C✝ : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f g : α →ᵇ β
x : α
⊢ ↑C * dist (↑f x) (↑g x) ≤ ↑C * dist f g
[PROOFSTEP]
gcongr
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g✝ : α →ᵇ β
x✝ : α
C✝ : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f g : α →ᵇ β
x : α
⊢ dist (↑f x) (↑g x) ≤ dist f g
[PROOFSTEP]
apply dist_coe_le_dist
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g : α →ᵇ β
h : δ →ᵇ β
⊢ ∃ C,
    ∀ (x y : δ),
      dist (ContinuousMap.toFun (ContinuousMap.mk (Function.extend ↑f ↑g ↑h)) x)
          (ContinuousMap.toFun (ContinuousMap.mk (Function.extend ↑f ↑g ↑h)) y) ≤
        C
[PROOFSTEP]
rw [← bounded_range_iff, range_extend f.injective, Metric.bounded_union]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g : α →ᵇ β
h : δ →ᵇ β
⊢ Metric.Bounded (range ↑g) ∧ Metric.Bounded (↑h '' (range ↑f)ᶜ)
[PROOFSTEP]
exact ⟨g.bounded_range, h.bounded_image _⟩
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (extend f g₁ h₁) (extend f g₂ h₂) = max (dist g₁ g₂) (dist (restrict h₁ (range ↑f)ᶜ) (restrict h₂ (range ↑f)ᶜ))
[PROOFSTEP]
refine' le_antisymm ((dist_le <| le_max_iff.2 <| Or.inl dist_nonneg).2 fun x => _) (max_le _ _)
[GOAL]
case refine'_1
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
⊢ dist (↑(extend f g₁ h₁) x) (↑(extend f g₂ h₂) x) ≤
    max (dist g₁ g₂) (dist (restrict h₁ (range ↑f)ᶜ) (restrict h₂ (range ↑f)ᶜ))
[PROOFSTEP]
rcases _root_.em (∃ y, f y = x) with (⟨x, rfl⟩ | hx)
[GOAL]
case refine'_1.inl.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (↑(extend f g₁ h₁) (↑f x)) (↑(extend f g₂ h₂) (↑f x)) ≤
    max (dist g₁ g₂) (dist (restrict h₁ (range ↑f)ᶜ) (restrict h₂ (range ↑f)ᶜ))
[PROOFSTEP]
simp only [extend_apply]
[GOAL]
case refine'_1.inl.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (↑g₁ x) (↑g₂ x) ≤ max (dist g₁ g₂) (dist (restrict h₁ (range ↑f)ᶜ) (restrict h₂ (range ↑f)ᶜ))
[PROOFSTEP]
exact (dist_coe_le_dist x).trans (le_max_left _ _)
[GOAL]
case refine'_1.inr
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ y, ↑f y = x
⊢ dist (↑(extend f g₁ h₁) x) (↑(extend f g₂ h₂) x) ≤
    max (dist g₁ g₂) (dist (restrict h₁ (range ↑f)ᶜ) (restrict h₂ (range ↑f)ᶜ))
[PROOFSTEP]
simp only [extend_apply' hx]
[GOAL]
case refine'_1.inr
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ y, ↑f y = x
⊢ dist (↑h₁ x) (↑h₂ x) ≤ max (dist g₁ g₂) (dist (restrict h₁ (range ↑f)ᶜ) (restrict h₂ (range ↑f)ᶜ))
[PROOFSTEP]
lift x to ((range f)ᶜ : Set δ) using hx
[GOAL]
case refine'_1.inr.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : { x // x ∈ (range ↑f)ᶜ }
⊢ dist (↑h₁ ↑x) (↑h₂ ↑x) ≤ max (dist g₁ g₂) (dist (restrict h₁ (range ↑f)ᶜ) (restrict h₂ (range ↑f)ᶜ))
[PROOFSTEP]
calc
  dist (h₁ x) (h₂ x) = dist (h₁.restrict (range f)ᶜ x) (h₂.restrict (range f)ᶜ x) := rfl
  _ ≤ dist (h₁.restrict (range f)ᶜ) (h₂.restrict (range f)ᶜ) := (dist_coe_le_dist x)
  _ ≤ _ := le_max_right _ _
[GOAL]
case refine'_2
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
[PROOFSTEP]
refine' (dist_le dist_nonneg).2 fun x => _
[GOAL]
case refine'_2
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (↑g₁ x) (↑g₂ x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
[PROOFSTEP]
rw [← extend_apply f g₁ h₁, ← extend_apply f g₂ h₂]
[GOAL]
case refine'_2
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (↑(extend f g₁ h₁) (↑f x)) (↑(extend f g₂ h₂) (↑f x)) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
[PROOFSTEP]
exact dist_coe_le_dist _
[GOAL]
case refine'_3
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (restrict h₁ (range ↑f)ᶜ) (restrict h₂ (range ↑f)ᶜ) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
[PROOFSTEP]
refine' (dist_le dist_nonneg).2 fun x => _
[GOAL]
case refine'_3
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : ↑(range ↑f)ᶜ
⊢ dist (↑(restrict h₁ (range ↑f)ᶜ) x) (↑(restrict h₂ (range ↑f)ᶜ) x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
[PROOFSTEP]
calc
  dist (h₁ x) (h₂ x) = dist (extend f g₁ h₁ x) (extend f g₂ h₂ x) := by
    rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]
  _ ≤ _ := dist_coe_le_dist _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : ↑(range ↑f)ᶜ
⊢ dist (↑h₁ ↑x) (↑h₂ ↑x) = dist (↑(extend f g₁ h₁) ↑x) (↑(extend f g₂ h₂) ↑x)
[PROOFSTEP]
rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
h : δ →ᵇ β
g₁ g₂ : α →ᵇ β
⊢ dist (extend f g₁ h) (extend f g₂ h) = dist g₁ g₂
[PROOFSTEP]
simp [dist_nonneg]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : Equicontinuous fun x => ↑↑x
⊢ IsCompact A
[PROOFSTEP]
simp_rw [Equicontinuous, Metric.equicontinuousAt_iff_pair] at H 
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
⊢ IsCompact A
[PROOFSTEP]
refine' isCompact_of_totallyBounded_isClosed _ closed
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
⊢ TotallyBounded A
[PROOFSTEP]
refine' totallyBounded_of_finite_discretization fun ε ε0 => _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
[PROOFSTEP]
rcases exists_between ε0 with ⟨ε₁, ε₁0, εε₁⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
[PROOFSTEP]
let ε₂ :=
  ε₁ / 2 /
    2
      /- We have to find a finite discretization of `u`, i.e., finite information
          that is sufficient to reconstruct `u` up to `ε`. This information will be
          provided by the values of `u` on a sufficiently dense set `tα`,
          slightly translated to fit in a finite `ε₂`-dense set `tβ` in the image. Such
          sets exist by compactness of the source and range. Then, to check that these
          data determine the function up to `ε`, one uses the control on the modulus of
          continuity to extend the closeness on tα to closeness everywhere. -/
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
[PROOFSTEP]
have ε₂0 : ε₂ > 0 := half_pos (half_pos ε₁0)
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
[PROOFSTEP]
have : ∀ x : α, ∃ U, x ∈ U ∧ IsOpen U ∧ ∀ (y) (_ : y ∈ U) (z) (_ : z ∈ U) {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂ :=
  fun x =>
  let ⟨U, nhdsU, hU⟩ := H x _ ε₂0
  let ⟨V, VU, openV, xV⟩ := _root_.mem_nhds_iff.1 nhdsU
  ⟨V, xV, openV, fun y hy z hz f hf => hU y (VU hy) z (VU hz) ⟨f, hf⟩⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
this :
  ∀ (x : α),
    ∃ U, x ∈ U ∧ IsOpen U ∧ ∀ (y : α), y ∈ U → ∀ (z : α), z ∈ U → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
[PROOFSTEP]
choose U hU using this
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
[PROOFSTEP]
rcases isCompact_univ.elim_finite_subcover_image (fun x _ => (hU x).2.1) fun x _ =>
    mem_biUnion (mem_univ _) (hU x).1 with
  ⟨tα, _, ⟨_⟩, htα⟩
    -- `tα: Set α`, `htα : univ ⊆ ⋃x ∈ tα, U x`
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝ : Fintype ↑tα
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
[PROOFSTEP]
rcases@finite_cover_balls_of_compact β _ _ isCompact_univ _ ε₂0 with
  ⟨tβ, _, ⟨_⟩, htβ⟩
    -- `tβ : Set β`, `htβ : univ ⊆ ⋃y ∈ tβ, ball y ε₂`
      -- Associate to every point `y` in the space a nearby point `F y` in `tβ`
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
[PROOFSTEP]
choose F hF using fun y =>
  show ∃ z ∈ tβ, dist y z < ε₂ by
    simpa using
      htβ
        (mem_univ y)
          -- `F : β → β`, `hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂`
            /- Associate to every function a discrete approximation, mapping each point in `tα`
              to a point in `tβ` close to its true image by the function. -/
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
y : β
⊢ ∃ z, z ∈ tβ ∧ dist y z < ε₂
[PROOFSTEP]
simpa using
  htβ
    (mem_univ y)
      -- `F : β → β`, `hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂`
        /- Associate to every function a discrete approximation, mapping each point in `tα`
          to a point in `tβ` close to its true image by the function. -/
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
[PROOFSTEP]
refine' ⟨tα → tβ, by infer_instance, fun f a => ⟨F (f.1 a), (hF (f.1 a)).1⟩, _⟩
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
⊢ Fintype (↑tα → ↑tβ)
[PROOFSTEP]
infer_instance
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
⊢ ∀ (x y : ↑A),
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) x =
        (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) y →
      dist ↑x ↑y < ε
[PROOFSTEP]
rintro ⟨f, hf⟩ ⟨g, hg⟩ f_eq_g
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.mk
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := f, property := hf } =
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := g, property := hg }
⊢ dist ↑{ val := f, property := hf } ↑{ val := g, property := hg } < ε
[PROOFSTEP]
refine' lt_of_le_of_lt ((dist_le <| le_of_lt ε₁0).2 fun x => _) εε₁
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.mk
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := f, property := hf } =
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := g, property := hg }
x : α
⊢ dist (↑↑{ val := f, property := hf } x) (↑↑{ val := g, property := hg } x) ≤ ε₁
[PROOFSTEP]
obtain ⟨x', x'tα, hx'⟩ := mem_iUnion₂.1 (htα (mem_univ x))
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro.intro
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := f, property := hf } =
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := g, property := hg }
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (↑↑{ val := f, property := hf } x) (↑↑{ val := g, property := hg } x) ≤ ε₁
[PROOFSTEP]
calc
  dist (f x) (g x) ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') := dist_triangle4_right _ _ _ _
  _ ≤ ε₂ + ε₂ + ε₁ / 2 := by
    refine' le_of_lt (add_lt_add (add_lt_add _ _) _)
    · exact (hU x').2.2 _ hx' _ (hU x').1 hf
    · exact (hU x').2.2 _ hx' _ (hU x').1 hg
    · have F_f_g : F (f x') = F (g x') := (congr_arg (fun f : tα → tβ => (f ⟨x', x'tα⟩ : β)) f_eq_g : _)
      calc
        dist (f x') (g x') ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) := dist_triangle_right _ _ _
        _ = dist (f x') (F (f x')) + dist (g x') (F (g x')) := by rw [F_f_g]
        _ < ε₂ + ε₂ := (add_lt_add (hF (f x')).2 (hF (g x')).2)
        _ = ε₁ / 2 := add_halves _
  _ = ε₁ := by rw [add_halves, add_halves]
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := f, property := hf } =
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := g, property := hg }
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (↑f x) (↑f x') + dist (↑g x) (↑g x') + dist (↑f x') (↑g x') ≤ ε₂ + ε₂ + ε₁ / 2
[PROOFSTEP]
refine' le_of_lt (add_lt_add (add_lt_add _ _) _)
[GOAL]
case refine'_1
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := f, property := hf } =
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := g, property := hg }
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (↑f x) (↑f x') < ε₂
[PROOFSTEP]
exact (hU x').2.2 _ hx' _ (hU x').1 hf
[GOAL]
case refine'_2
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := f, property := hf } =
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := g, property := hg }
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (↑g x) (↑g x') < ε₂
[PROOFSTEP]
exact (hU x').2.2 _ hx' _ (hU x').1 hg
[GOAL]
case refine'_3
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := f, property := hf } =
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := g, property := hg }
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (↑f x') (↑g x') < ε₁ / 2
[PROOFSTEP]
have F_f_g : F (f x') = F (g x') := (congr_arg (fun f : tα → tβ => (f ⟨x', x'tα⟩ : β)) f_eq_g : _)
[GOAL]
case refine'_3
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := f, property := hf } =
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := g, property := hg }
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
F_f_g : F (↑f x') = F (↑g x')
⊢ dist (↑f x') (↑g x') < ε₁ / 2
[PROOFSTEP]
calc
  dist (f x') (g x') ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) := dist_triangle_right _ _ _
  _ = dist (f x') (F (f x')) + dist (g x') (F (g x')) := by rw [F_f_g]
  _ < ε₂ + ε₂ := (add_lt_add (hF (f x')).2 (hF (g x')).2)
  _ = ε₁ / 2 := add_halves _
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := f, property := hf } =
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := g, property := hg }
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
F_f_g : F (↑f x') = F (↑g x')
⊢ dist (↑f x') (F (↑f x')) + dist (↑g x') (F (↑f x')) = dist (↑f x') (F (↑f x')) + dist (↑g x') (F (↑g x'))
[PROOFSTEP]
rw [F_f_g]
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α) (ε : ℝ),
    ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : α), x ∈ U → ∀ (x' : α), x' ∈ U → ∀ (i : ↑A), dist (↑↑i x) (↑↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧ IsOpen (U x) ∧ ∀ (y : α), y ∈ U x → ∀ (z : α), z ∈ U x → ∀ {f : α →ᵇ β}, f ∈ A → dist (↑f y) (↑f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
htα : univ ⊆ ⋃ (i : α) (_ : i ∈ tα), U i
a✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
htβ : univ ⊆ ⋃ (x : β) (_ : x ∈ tβ), ball x ε₂
a✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := f, property := hf } =
    (fun f a => { val := F (↑↑f ↑a), property := (_ : F (↑↑f ↑a) ∈ tβ) }) { val := g, property := hg }
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ ε₂ + ε₂ + ε₁ / 2 = ε₁
[PROOFSTEP]
rw [add_halves, add_halves]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
⊢ IsCompact A
[PROOFSTEP]
have M : LipschitzWith 1 (↑) := LipschitzWith.subtype_val s
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
⊢ IsCompact A
[PROOFSTEP]
let F : (α →ᵇ s) → α →ᵇ β := comp (↑) M
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
⊢ IsCompact A
[PROOFSTEP]
refine' isCompact_of_isClosed_subset ((_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed fun f hf => _
[GOAL]
case refine'_1
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
⊢ IsCompact (F ⁻¹' A)
[PROOFSTEP]
haveI : CompactSpace s := isCompact_iff_compactSpace.1 hs
[GOAL]
case refine'_1
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
this : CompactSpace ↑s
⊢ IsCompact (F ⁻¹' A)
[PROOFSTEP]
refine' arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) _
[GOAL]
case refine'_1
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
this : CompactSpace ↑s
⊢ Equicontinuous fun x => ↑↑x
[PROOFSTEP]
rw [uniformEmbedding_subtype_val.toUniformInducing.equicontinuous_iff]
[GOAL]
case refine'_1
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
this : CompactSpace ↑s
⊢ Equicontinuous ((fun x x_1 => x ∘ x_1) Subtype.val ∘ fun x => ↑↑x)
[PROOFSTEP]
exact H.comp (A.restrictPreimage F)
[GOAL]
case refine'_2
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f✝ g : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
⊢ f ∈ comp Subtype.val M '' (F ⁻¹' A)
[PROOFSTEP]
let g := codRestrict s f fun x => in_s f x hf
[GOAL]
case refine'_2
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ ↑s := codRestrict s f (_ : ∀ (x : α), ↑f x ∈ s)
⊢ f ∈ comp Subtype.val M '' (F ⁻¹' A)
[PROOFSTEP]
rw [show f = F g by ext; rfl] at hf ⊢
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ ↑s := codRestrict s f (_ : ∀ (x : α), ↑f x ∈ s)
⊢ f = F g
[PROOFSTEP]
ext
[GOAL]
case h
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ ↑s := codRestrict s f (_ : ∀ (x : α), ↑f x ∈ s)
x✝ : α
⊢ ↑f x✝ = ↑(F g) x✝
[PROOFSTEP]
rfl
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf✝ : f ∈ A
g : α →ᵇ ↑s := codRestrict s f (_ : ∀ (x : α), ↑f x ∈ s)
hf : F g ∈ A
⊢ f = F g
[PROOFSTEP]
ext
[GOAL]
case h
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf✝ : f ∈ A
g : α →ᵇ ↑s := codRestrict s f (_ : ∀ (x : α), ↑f x ∈ s)
hf : F g ∈ A
x✝ : α
⊢ ↑f x✝ = ↑(F g) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → ↑f x ∈ s
H : Equicontinuous fun x => ↑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf✝ : f ∈ A
g : α →ᵇ ↑s := codRestrict s f (_ : ∀ (x : α), ↑f x ∈ s)
hf : F g ∈ A
⊢ F g ∈ comp Subtype.val M '' (F ⁻¹' A)
[PROOFSTEP]
exact ⟨g, hf, rfl⟩
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
⊢ ∀ (x y : α),
    dist (↑(f.toContinuousMap + g.toContinuousMap) x) (↑(f.toContinuousMap + g.toContinuousMap) y) ≤
      ↑(LipschitzAdd.C β) *
        max (choose (_ : ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C))
          (choose (_ : ∃ C, ∀ (x y : α), dist (↑g x) (↑g y) ≤ C))
[PROOFSTEP]
intro x y
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
f g : α →ᵇ β
x y : α
⊢ dist (↑(f.toContinuousMap + g.toContinuousMap) x) (↑(f.toContinuousMap + g.toContinuousMap) y) ≤
    ↑(LipschitzAdd.C β) *
      max (choose (_ : ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C))
        (choose (_ : ∃ C, ∀ (x y : α), dist (↑g x) (↑g y) ≤ C))
[PROOFSTEP]
refine' le_trans (lipschitz_with_lipschitz_const_add ⟨f x, g x⟩ ⟨f y, g y⟩) _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
f g : α →ᵇ β
x y : α
⊢ ↑(LipschitzAdd.C ((fun a => β) x)) * dist (↑f x, ↑g x) (↑f y, ↑g y) ≤
    ↑(LipschitzAdd.C β) *
      max (choose (_ : ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C))
        (choose (_ : ∃ C, ∀ (x y : α), dist (↑g x) (↑g y) ≤ C))
[PROOFSTEP]
rw [Prod.dist_eq]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
f g : α →ᵇ β
x y : α
⊢ ↑(LipschitzAdd.C ((fun a => β) x)) *
      max (dist (↑f x, ↑g x).fst (↑f y, ↑g y).fst) (dist (↑f x, ↑g x).snd (↑f y, ↑g y).snd) ≤
    ↑(LipschitzAdd.C β) *
      max (choose (_ : ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C))
        (choose (_ : ∃ C, ∀ (x y : α), dist (↑g x) (↑g y) ≤ C))
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_left _ (LipschitzAdd.C β).coe_nonneg
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
f g : α →ᵇ β
x y : α
⊢ max (dist (↑f x, ↑g x).fst (↑f y, ↑g y).fst) (dist (↑f x, ↑g x).snd (↑f y, ↑g y).snd) ≤
    max (choose (_ : ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C)) (choose (_ : ∃ C, ∀ (x y : α), dist (↑g x) (↑g y) ≤ C))
[PROOFSTEP]
apply max_le_max
[GOAL]
case a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
f g : α →ᵇ β
x y : α
⊢ dist (↑f x, ↑g x).fst (↑f y, ↑g y).fst ≤ choose (_ : ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C)
case a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
f g : α →ᵇ β
x y : α
⊢ dist (↑f x, ↑g x).snd (↑f y, ↑g y).snd ≤ choose (_ : ∃ C, ∀ (x y : α), dist (↑g x) (↑g y) ≤ C)
[PROOFSTEP]
exact Classical.choose_spec f.bounded x y
[GOAL]
case a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
f g : α →ᵇ β
x y : α
⊢ dist (↑f x, ↑g x).snd (↑f y, ↑g y).snd ≤ choose (_ : ∃ C, ∀ (x y : α), dist (↑g x) (↑g y) ≤ C)
[PROOFSTEP]
exact Classical.choose_spec g.bounded x y
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ↑(nsmulRec 0 f) = 0 • ↑f
[PROOFSTEP]
rw [nsmulRec, zero_smul, coe_zero]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
n : ℕ
⊢ ↑(nsmulRec (n + 1) f) = (n + 1) • ↑f
[PROOFSTEP]
rw [nsmulRec, succ_nsmul, coe_add, coe_nsmulRec n]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f✝ g : α →ᵇ β
x : α
C : ℝ
n : ℕ
f : α →ᵇ β
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (n • f.toContinuousMap) x) (ContinuousMap.toFun (n • f.toContinuousMap) y) ≤ C
[PROOFSTEP]
simpa [coe_nsmulRec] using (nsmulRec n f).map_bounded'
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
⊢ LipschitzWith (LipschitzAdd.C β) fun p => p.fst + p.snd
[PROOFSTEP]
have C_nonneg := (LipschitzAdd.C β).coe_nonneg
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
⊢ LipschitzWith (LipschitzAdd.C β) fun p => p.fst + p.snd
[PROOFSTEP]
rw [lipschitzWith_iff_dist_le_mul]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
⊢ ∀ (x y : (α →ᵇ β) × (α →ᵇ β)), dist (x.fst + x.snd) (y.fst + y.snd) ≤ ↑(LipschitzAdd.C β) * dist x y
[PROOFSTEP]
rintro ⟨f₁, g₁⟩ ⟨f₂, g₂⟩
[GOAL]
case mk.mk
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
⊢ dist ((f₁, g₁).fst + (f₁, g₁).snd) ((f₂, g₂).fst + (f₂, g₂).snd) ≤ ↑(LipschitzAdd.C β) * dist (f₁, g₁) (f₂, g₂)
[PROOFSTEP]
rw [dist_le (mul_nonneg C_nonneg dist_nonneg)]
[GOAL]
case mk.mk
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
⊢ ∀ (x : α),
    dist (↑((f₁, g₁).fst + (f₁, g₁).snd) x) (↑((f₂, g₂).fst + (f₂, g₂).snd) x) ≤
      ↑(LipschitzAdd.C β) * dist (f₁, g₁) (f₂, g₂)
[PROOFSTEP]
intro x
[GOAL]
case mk.mk
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist (↑((f₁, g₁).fst + (f₁, g₁).snd) x) (↑((f₂, g₂).fst + (f₂, g₂).snd) x) ≤
    ↑(LipschitzAdd.C β) * dist (f₁, g₁) (f₂, g₂)
[PROOFSTEP]
refine' le_trans (lipschitz_with_lipschitz_const_add ⟨f₁ x, g₁ x⟩ ⟨f₂ x, g₂ x⟩) _
[GOAL]
case mk.mk
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ ↑(LipschitzAdd.C ((fun a => β) x)) * dist (↑f₁ x, ↑g₁ x) (↑f₂ x, ↑g₂ x) ≤ ↑(LipschitzAdd.C β) * dist (f₁, g₁) (f₂, g₂)
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_left _ C_nonneg
[GOAL]
case mk.mk
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist (↑f₁ x, ↑g₁ x) (↑f₂ x, ↑g₂ x) ≤ dist (f₁, g₁) (f₂, g₂)
[PROOFSTEP]
apply max_le_max
[GOAL]
case mk.mk.a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist (↑f₁ x, ↑g₁ x).fst (↑f₂ x, ↑g₂ x).fst ≤ dist (f₁, g₁).fst (f₂, g₂).fst
[PROOFSTEP]
exact dist_coe_le_dist x
[GOAL]
case mk.mk.a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist (↑f₁ x, ↑g₁ x).snd (↑f₂ x, ↑g₂ x).snd ≤ dist (f₁, g₁).snd (f₂, g₂).snd
[PROOFSTEP]
exact dist_coe_le_dist x
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ∀ (x y : α →ᵇ β),
    ZeroHom.toFun { toFun := toContinuousMap, map_zero' := (_ : 0.toContinuousMap = 0.toContinuousMap) } (x + y) =
      ZeroHom.toFun { toFun := toContinuousMap, map_zero' := (_ : 0.toContinuousMap = 0.toContinuousMap) } x +
        ZeroHom.toFun { toFun := toContinuousMap, map_zero' := (_ : 0.toContinuousMap = 0.toContinuousMap) } y
[PROOFSTEP]
intros
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
x✝ y✝ : α →ᵇ β
⊢ ZeroHom.toFun { toFun := toContinuousMap, map_zero' := (_ : 0.toContinuousMap = 0.toContinuousMap) } (x✝ + y✝) =
    ZeroHom.toFun { toFun := toContinuousMap, map_zero' := (_ : 0.toContinuousMap = 0.toContinuousMap) } x✝ +
      ZeroHom.toFun { toFun := toContinuousMap, map_zero' := (_ : 0.toContinuousMap = 0.toContinuousMap) } y✝
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
x✝ y✝ : α →ᵇ β
a✝ : α
⊢ ↑(ZeroHom.toFun { toFun := toContinuousMap, map_zero' := (_ : 0.toContinuousMap = 0.toContinuousMap) } (x✝ + y✝)) a✝ =
    ↑(ZeroHom.toFun { toFun := toContinuousMap, map_zero' := (_ : 0.toContinuousMap = 0.toContinuousMap) } x✝ +
          ZeroHom.toFun { toFun := toContinuousMap, map_zero' := (_ : 0.toContinuousMap = 0.toContinuousMap) } y✝)
      a✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddCommMonoid β
inst✝ : LipschitzAdd β
src✝ : AddMonoid (α →ᵇ β) := addMonoid
f g : α →ᵇ β
⊢ f + g = g + f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddCommMonoid β
inst✝ : LipschitzAdd β
src✝ : AddMonoid (α →ᵇ β) := addMonoid
f g : α →ᵇ β
x✝ : α
⊢ ↑(f + g) x✝ = ↑(g + f) x✝
[PROOFSTEP]
simp [add_comm]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddCommMonoid β
inst✝ : LipschitzAdd β
ι : Type u_2
s : Finset ι
f : ι → α →ᵇ β
a : α
⊢ ↑(∑ i in s, f i) a = ∑ i in s, ↑(f i) a
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
f : α →ᵇ β
⊢ ‖f‖ = sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖↑f x‖ ≤ C}
[PROOFSTEP]
simp [norm_def, BoundedContinuousFunction.dist_eq]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
h : Nonempty α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖↑f x‖ ≤ C}
[PROOFSTEP]
obtain ⟨a⟩ := h
[GOAL]
case intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖↑f x‖ ≤ C}
[PROOFSTEP]
rw [norm_eq]
[GOAL]
case intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖↑f x‖ ≤ C} = sInf {C | ∀ (x : α), ‖↑f x‖ ≤ C}
[PROOFSTEP]
congr
[GOAL]
case intro.e_a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
⊢ {C | 0 ≤ C ∧ ∀ (x : α), ‖↑f x‖ ≤ C} = {C | ∀ (x : α), ‖↑f x‖ ≤ C}
[PROOFSTEP]
ext
[GOAL]
case intro.e_a.h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
x✝ : ℝ
⊢ x✝ ∈ {C | 0 ≤ C ∧ ∀ (x : α), ‖↑f x‖ ≤ C} ↔ x✝ ∈ {C | ∀ (x : α), ‖↑f x‖ ≤ C}
[PROOFSTEP]
simp only [mem_setOf_eq, and_iff_right_iff_imp]
[GOAL]
case intro.e_a.h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
x✝ : ℝ
⊢ (∀ (x : α), ‖↑f x‖ ≤ x✝) → 0 ≤ x✝
[PROOFSTEP]
exact fun h' => le_trans (norm_nonneg (f a)) (h' a)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x✝ : α
C : ℝ
x : α
⊢ ‖↑f x‖ = dist (↑f x) (↑0 x)
[PROOFSTEP]
simp [dist_zero_right]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
C0 : 0 ≤ C
⊢ ‖f‖ ≤ C ↔ ∀ (x : α), ‖↑f x‖ ≤ C
[PROOFSTEP]
simpa using @dist_le _ _ _ _ f 0 _ C0
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ ≤ M ↔ ∀ (x : α), ‖↑f x‖ ≤ M
[PROOFSTEP]
simp_rw [norm_def, ← dist_zero_right]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ dist f 0 ≤ M ↔ ∀ (x : α), dist (↑f x) 0 ≤ M
[PROOFSTEP]
exact dist_le_iff_of_nonempty
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖↑f x‖ < M
[PROOFSTEP]
simp_rw [norm_def, ← dist_zero_right]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ dist f 0 < M ↔ ∀ (x : α), dist (↑f x) 0 < M
[PROOFSTEP]
exact dist_lt_iff_of_compact M0
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖↑f x‖ < M
[PROOFSTEP]
simp_rw [norm_def, ← dist_zero_right]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
⊢ dist f 0 < M ↔ ∀ (x : α), dist (↑f x) 0 < M
[PROOFSTEP]
exact dist_lt_iff_of_nonempty_compact
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ‖normComp f‖ = ‖f‖
[PROOFSTEP]
simp only [norm_eq, coe_normComp, norm_norm, Function.comp]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ‖f‖ = ⨆ (x : α), ‖↑f x‖
[PROOFSTEP]
simp_rw [norm_def, dist_eq_iSup, coe_zero, Pi.zero_apply, dist_zero_right]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
inst✝² : Nonempty α
inst✝¹ : One β
inst✝ : NormOneClass β
⊢ ‖1‖ = 1
[PROOFSTEP]
simp only [norm_eq_iSup_norm, coe_one, Pi.one_apply, norm_one, ciSup_const]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
f g : α →ᵇ β
x : α
⊢ ‖(↑f - ↑g) x‖ ≤ ‖f‖ + ‖g‖
[PROOFSTEP]
simp only [sub_eq_add_neg]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
f g : α →ᵇ β
x : α
⊢ ‖(↑f + -↑g) x‖ ≤ ‖f‖ + ‖g‖
[PROOFSTEP]
exact le_trans (norm_add_le _ _) (add_le_add (f.norm_coe_le_norm x) <| norm_neg ((⇑g) x) ▸ g.norm_coe_le_norm x)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
n : ℕ
⊢ ↑(zsmulRec (Int.ofNat n) f) = Int.ofNat n • ↑f
[PROOFSTEP]
rw [zsmulRec, Int.ofNat_eq_coe, coe_nsmulRec, coe_nat_zsmul]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
n : ℕ
⊢ ↑(zsmulRec (Int.negSucc n) f) = Int.negSucc n • ↑f
[PROOFSTEP]
rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmulRec]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
n : ℤ
f : α →ᵇ β
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (n • f.toContinuousMap) x) (ContinuousMap.toFun (n • f.toContinuousMap) y) ≤ C
[PROOFSTEP]
simpa using (zsmulRec n f).map_bounded'
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
⊢ dist f g = ‖f - g‖
[PROOFSTEP]
simp only [norm_eq, dist_eq, dist_eq_norm, sub_apply]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ⨆ (x : α), ‖↑f x‖ = ↑(⨆ (x : α), ‖↑f x‖₊)
[PROOFSTEP]
simp_rw [val_eq_coe, NNReal.coe_iSup, coe_nnnorm]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ‖↑f x - ↑g x‖ ≤ dist f g
[PROOFSTEP]
rw [dist_eq_norm]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ‖↑f x - ↑g x‖ ≤ ‖f - g‖
[PROOFSTEP]
exact (f - g).norm_coe_le_norm x
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
inst✝ : TopologicalSpace γ
f : α →ᵇ β
g : C(γ, α)
⊢ ↑1 * dist f 0 ≤ ‖f‖
[PROOFSTEP]
rw [NNReal.coe_one, one_mul, dist_zero_right]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α →ᵇ β
b : ℝ
hb : ∀ (x y : α), dist (↑f x) (↑f y) ≤ b
x y : α
⊢ dist (ContinuousMap.toFun (c • f.toContinuousMap) x) (ContinuousMap.toFun (c • f.toContinuousMap) y) ≤ dist c 0 * b
[PROOFSTEP]
refine' (dist_smul_pair c (f x) (f y)).trans _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α →ᵇ β
b : ℝ
hb : ∀ (x y : α), dist (↑f x) (↑f y) ≤ b
x y : α
⊢ dist c 0 * dist (↑f x) (↑f y) ≤ dist c 0 * b
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_left _ dist_nonneg
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α →ᵇ β
b : ℝ
hb : ∀ (x y : α), dist (↑f x) (↑f y) ≤ b
x y : α
⊢ dist (↑f x) (↑f y) ≤ b
[PROOFSTEP]
exact hb x y
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
⊢ dist (c • f₁) (c • f₂) ≤ dist c 0 * dist f₁ f₂
[PROOFSTEP]
rw [dist_le (mul_nonneg dist_nonneg dist_nonneg)]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
⊢ ∀ (x : α), dist (↑(c • f₁) x) (↑(c • f₂) x) ≤ dist c 0 * dist f₁ f₂
[PROOFSTEP]
intro x
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
x : α
⊢ dist (↑(c • f₁) x) (↑(c • f₂) x) ≤ dist c 0 * dist f₁ f₂
[PROOFSTEP]
refine' (dist_smul_pair c (f₁ x) (f₂ x)).trans _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
x : α
⊢ dist c 0 * dist (↑f₁ x) (↑f₂ x) ≤ dist c 0 * dist f₁ f₂
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left (dist_coe_le_dist x) dist_nonneg
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
⊢ dist (c₁ • f) (c₂ • f) ≤ dist c₁ c₂ * dist f 0
[PROOFSTEP]
rw [dist_le (mul_nonneg dist_nonneg dist_nonneg)]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
⊢ ∀ (x : α), dist (↑(c₁ • f) x) (↑(c₂ • f) x) ≤ dist c₁ c₂ * dist f 0
[PROOFSTEP]
intro x
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
x : α
⊢ dist (↑(c₁ • f) x) (↑(c₂ • f) x) ≤ dist c₁ c₂ * dist f 0
[PROOFSTEP]
refine' (dist_pair_smul c₁ c₂ (f x)).trans _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
x : α
⊢ dist c₁ c₂ * dist (↑f x) 0 ≤ dist c₁ c₂ * dist f 0
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_left _ dist_nonneg
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
x : α
⊢ dist (↑f x) 0 ≤ dist f 0
[PROOFSTEP]
convert dist_coe_le_dist (β := β) x
[GOAL]
case h.e'_3.h.e'_4
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
x : α
⊢ 0 = ↑0 x
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
c : 𝕜
f : α →ᵇ β
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
[PROOFSTEP]
refine' norm_ofNormedAddCommGroup_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
c : 𝕜
f : α →ᵇ β
⊢ ∀ (x : α), ‖(c • ↑f.toContinuousMap) x‖ ≤ ‖c‖ * ‖f‖
[PROOFSTEP]
exact fun x => norm_smul c (f x) ▸ mul_le_mul_of_nonneg_left (f.norm_coe_le_norm _) (norm_nonneg _)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝¹ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g✝ : β →L[𝕜] γ
f g : α →ᵇ β
⊢ (fun f =>
        ofNormedAddCommGroup (↑g✝ ∘ ↑f) (_ : Continuous (↑g✝ ∘ ↑f)) (‖g✝‖ * ‖f‖)
          (_ : ∀ (x : α), ‖↑g✝ (↑f x)‖ ≤ ‖g✝‖ * ‖f‖))
      (f + g) =
    (fun f =>
          ofNormedAddCommGroup (↑g✝ ∘ ↑f) (_ : Continuous (↑g✝ ∘ ↑f)) (‖g✝‖ * ‖f‖)
            (_ : ∀ (x : α), ‖↑g✝ (↑f x)‖ ≤ ‖g✝‖ * ‖f‖))
        f +
      (fun f =>
          ofNormedAddCommGroup (↑g✝ ∘ ↑f) (_ : Continuous (↑g✝ ∘ ↑f)) (‖g✝‖ * ‖f‖)
            (_ : ∀ (x : α), ‖↑g✝ (↑f x)‖ ≤ ‖g✝‖ * ‖f‖))
        g
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝¹ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g✝ : β →L[𝕜] γ
f g : α →ᵇ β
x✝ : α
⊢ ↑((fun f =>
            ofNormedAddCommGroup (↑g✝ ∘ ↑f) (_ : Continuous (↑g✝ ∘ ↑f)) (‖g✝‖ * ‖f‖)
              (_ : ∀ (x : α), ‖↑g✝ (↑f x)‖ ≤ ‖g✝‖ * ‖f‖))
          (f + g))
      x✝ =
    ↑((fun f =>
              ofNormedAddCommGroup (↑g✝ ∘ ↑f) (_ : Continuous (↑g✝ ∘ ↑f)) (‖g✝‖ * ‖f‖)
                (_ : ∀ (x : α), ‖↑g✝ (↑f x)‖ ≤ ‖g✝‖ * ‖f‖))
            f +
          (fun f =>
              ofNormedAddCommGroup (↑g✝ ∘ ↑f) (_ : Continuous (↑g✝ ∘ ↑f)) (‖g✝‖ * ‖f‖)
                (_ : ∀ (x : α), ‖↑g✝ (↑f x)‖ ≤ ‖g✝‖ * ‖f‖))
            g)
      x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
c : 𝕜
f : α →ᵇ β
⊢ AddHom.toFun
      {
        toFun := fun f =>
          ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
            (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖),
        map_add' :=
          (_ :
            ∀ (f g_1 : α →ᵇ β),
              (fun f =>
                    ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                      (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                  (f + g_1) =
                (fun f =>
                      ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                        (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                    f +
                  (fun f =>
                      ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                        (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                    g_1) }
      (c • f) =
    ↑(RingHom.id 𝕜) c •
      AddHom.toFun
        {
          toFun := fun f =>
            ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
              (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖),
          map_add' :=
            (_ :
              ∀ (f g_1 : α →ᵇ β),
                (fun f =>
                      ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                        (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                    (f + g_1) =
                  (fun f =>
                        ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                          (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                      f +
                    (fun f =>
                        ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                          (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                      g_1) }
        f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
c : 𝕜
f : α →ᵇ β
x✝ : α
⊢ ↑(AddHom.toFun
          {
            toFun := fun f =>
              ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖),
            map_add' :=
              (_ :
                ∀ (f g_1 : α →ᵇ β),
                  (fun f =>
                        ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                          (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                      (f + g_1) =
                    (fun f =>
                          ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                            (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                        f +
                      (fun f =>
                          ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                            (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                        g_1) }
          (c • f))
      x✝ =
    ↑(↑(RingHom.id 𝕜) c •
          AddHom.toFun
            {
              toFun := fun f =>
                ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                  (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖),
              map_add' :=
                (_ :
                  ∀ (f g_1 : α →ᵇ β),
                    (fun f =>
                          ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                            (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                        (f + g_1) =
                      (fun f =>
                            ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                              (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                          f +
                        (fun f =>
                            ofNormedAddCommGroup (↑g ∘ ↑f) (_ : Continuous (↑g ∘ ↑f)) (‖g‖ * ‖f‖)
                              (_ : ∀ (x : α), ‖↑g (↑f x)‖ ≤ ‖g‖ * ‖f‖))
                          g_1) }
            f)
      x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : α →ᵇ β
x : α
⊢ ‖(↑g ∘ ↑f) x‖ ≤ ‖g‖ * ‖f‖
[PROOFSTEP]
exact g.le_op_norm_of_le (f.norm_coe_le_norm x)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
R : Type u_2
inst✝ : SeminormedRing R
f : α →ᵇ R
⊢ ↑(npowRec 0 f) = ↑f ^ 0
[PROOFSTEP]
rw [npowRec, pow_zero, coe_one]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
R : Type u_2
inst✝ : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ↑(npowRec (n + 1) f) = ↑f ^ (n + 1)
[PROOFSTEP]
rw [npowRec, pow_succ, coe_mul, coe_npowRec f n]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
R : Type u_2
inst✝ : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (f.toContinuousMap ^ n) x) (ContinuousMap.toFun (f.toContinuousMap ^ n) y) ≤ C
[PROOFSTEP]
simpa [coe_npowRec] using (npowRec n f).map_bounded'
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedRing γ
inst✝ : NormedAlgebra 𝕜 γ
f g : α →ᵇ γ
x : α
c k : 𝕜
a : α
⊢ ↑(↑(algebraMap 𝕜 (α →ᵇ γ)) k) a = k • 1
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedRing γ
inst✝ : NormedAlgebra 𝕜 γ
f g : α →ᵇ γ
x : α
c k : 𝕜
a : α
⊢ ↑(k • 1) a = k • 1
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α✝ : Type u
β : Type v
γ : Type w
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
⊢ ↑f x ≤ nndist f 0
[PROOFSTEP]
have key : nndist (f x) ((0 : α →ᵇ ℝ≥0) x) ≤ nndist f 0 := @dist_coe_le_dist α ℝ≥0 _ _ f 0 x
[GOAL]
F : Type u_1
α✝ : Type u
β : Type v
γ : Type w
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (↑f x) (↑0 x) ≤ nndist f 0
⊢ ↑f x ≤ nndist f 0
[PROOFSTEP]
simp only [coe_zero, Pi.zero_apply] at key 
[GOAL]
F : Type u_1
α✝ : Type u
β : Type v
γ : Type w
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (↑f x) 0 ≤ nndist f 0
⊢ ↑f x ≤ nndist f 0
[PROOFSTEP]
rwa [NNReal.nndist_zero_eq_val' (f x)] at key 
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
inst✝³ : StarAddMonoid β
inst✝² : NormedStarGroup β
inst✝¹ : NormedSpace 𝕜 β
inst✝ : StarModule 𝕜 β
f : α →ᵇ β
⊢ ‖star f‖ = ‖f‖
[PROOFSTEP]
simp only [norm_eq, star_apply, norm_star]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
⊢ ∀ {x : α →ᵇ β}, ‖star x * x‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
intro f
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
⊢ ‖star f * f‖ = ‖f‖ * ‖f‖
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
⊢ ‖star f * f‖ ≤ ‖f‖ * ‖f‖
[PROOFSTEP]
rw [← sq, norm_le (sq_nonneg _)]
[GOAL]
case refine'_1
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
⊢ ∀ (x : α), ‖↑(star f * f) x‖ ≤ ‖f‖ ^ 2
[PROOFSTEP]
dsimp [star_apply]
[GOAL]
case refine'_1
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
⊢ ∀ (x : α), ‖star (↑f x) * ↑f x‖ ≤ ‖f‖ ^ 2
[PROOFSTEP]
intro x
[GOAL]
case refine'_1
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
x : α
⊢ ‖star (↑f x) * ↑f x‖ ≤ ‖f‖ ^ 2
[PROOFSTEP]
rw [CstarRing.norm_star_mul_self, ← sq]
[GOAL]
case refine'_1
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
x : α
⊢ ‖↑f x‖ ^ 2 ≤ ‖f‖ ^ 2
[PROOFSTEP]
refine' sq_le_sq' _ _
[GOAL]
case refine'_1.refine'_1
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
x : α
⊢ -‖f‖ ≤ ‖↑f x‖
[PROOFSTEP]
linarith [norm_nonneg (f x), norm_nonneg f]
[GOAL]
case refine'_1.refine'_2
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
x : α
⊢ ‖↑f x‖ ≤ ‖f‖
[PROOFSTEP]
exact norm_coe_le_norm f x
[GOAL]
case refine'_2
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖
[PROOFSTEP]
rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _), norm_le (Real.sqrt_nonneg _)]
[GOAL]
case refine'_2
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
⊢ ∀ (x : α), ‖↑f x‖ ≤ Real.sqrt ‖star f * f‖
[PROOFSTEP]
intro x
[GOAL]
case refine'_2
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
x : α
⊢ ‖↑f x‖ ≤ Real.sqrt ‖star f * f‖
[PROOFSTEP]
rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CstarRing.norm_star_mul_self]
[GOAL]
case refine'_2
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CstarRing β
f : α →ᵇ β
x : α
⊢ ‖star (↑f x) * ↑f x‖ ≤ ‖star f * f‖
[PROOFSTEP]
exact norm_coe_le_norm (star f * f) x
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
⊢ Injective fun f => f.toFun
[PROOFSTEP]
simp [Injective]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝ : PartialOrder (α →ᵇ β) := partialOrder
f g : α →ᵇ β
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊓ ↑g t) x)
          (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊓ ↑g t) y) ≤
        C
[PROOFSTEP]
obtain ⟨C₁, hf⟩ := f.bounded
[GOAL]
case intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝ : PartialOrder (α →ᵇ β) := partialOrder
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (↑f x) (↑f y) ≤ C₁
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊓ ↑g t) x)
          (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊓ ↑g t) y) ≤
        C
[PROOFSTEP]
obtain ⟨C₂, hg⟩ := g.bounded
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝ : PartialOrder (α →ᵇ β) := partialOrder
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (↑f x) (↑f y) ≤ C₁
C₂ : ℝ
hg : ∀ (x y : α), dist (↑g x) (↑g y) ≤ C₂
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊓ ↑g t) x)
          (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊓ ↑g t) y) ≤
        C
[PROOFSTEP]
refine' ⟨C₁ + C₂, fun x y => _⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝ : PartialOrder (α →ᵇ β) := partialOrder
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (↑f x) (↑f y) ≤ C₁
C₂ : ℝ
hg : ∀ (x y : α), dist (↑g x) (↑g y) ≤ C₂
x y : α
⊢ dist (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊓ ↑g t) x)
      (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊓ ↑g t) y) ≤
    C₁ + C₂
[PROOFSTEP]
simp_rw [NormedAddCommGroup.dist_eq] at hf hg ⊢
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝ : PartialOrder (α →ᵇ β) := partialOrder
f g : α →ᵇ β
C₁ C₂ : ℝ
x y : α
hf : ∀ (x y : α), ‖↑f x - ↑f y‖ ≤ C₁
hg : ∀ (x y : α), ‖↑g x - ↑g y‖ ≤ C₂
⊢ ‖↑f x ⊓ ↑g x - ↑f y ⊓ ↑g y‖ ≤ C₁ + C₂
[PROOFSTEP]
exact (norm_inf_sub_inf_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _))
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝ : PartialOrder (α →ᵇ β) := partialOrder
f g : α →ᵇ β
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊔ ↑g t) x)
          (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊔ ↑g t) y) ≤
        C
[PROOFSTEP]
obtain ⟨C₁, hf⟩ := f.bounded
[GOAL]
case intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝ : PartialOrder (α →ᵇ β) := partialOrder
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (↑f x) (↑f y) ≤ C₁
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊔ ↑g t) x)
          (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊔ ↑g t) y) ≤
        C
[PROOFSTEP]
obtain ⟨C₂, hg⟩ := g.bounded
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝ : PartialOrder (α →ᵇ β) := partialOrder
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (↑f x) (↑f y) ≤ C₁
C₂ : ℝ
hg : ∀ (x y : α), dist (↑g x) (↑g y) ≤ C₂
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊔ ↑g t) x)
          (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊔ ↑g t) y) ≤
        C
[PROOFSTEP]
refine' ⟨C₁ + C₂, fun x y => _⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝ : PartialOrder (α →ᵇ β) := partialOrder
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (↑f x) (↑f y) ≤ C₁
C₂ : ℝ
hg : ∀ (x y : α), dist (↑g x) (↑g y) ≤ C₂
x y : α
⊢ dist (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊔ ↑g t) x)
      (ContinuousMap.toFun (ContinuousMap.mk fun t => ↑f t ⊔ ↑g t) y) ≤
    C₁ + C₂
[PROOFSTEP]
simp_rw [NormedAddCommGroup.dist_eq] at hf hg ⊢
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝ : PartialOrder (α →ᵇ β) := partialOrder
f g : α →ᵇ β
C₁ C₂ : ℝ
x y : α
hf : ∀ (x y : α), ‖↑f x - ↑f y‖ ≤ C₁
hg : ∀ (x y : α), ‖↑g x - ↑g y‖ ≤ C₂
⊢ ‖↑f x ⊔ ↑g x - ↑f y ⊔ ↑g y‖ ≤ C₁ + C₂
[PROOFSTEP]
exact (norm_sup_sub_sup_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _))
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝¹ : Lattice (α →ᵇ β) := lattice
src✝ : SeminormedAddCommGroup (α →ᵇ β) := seminormedAddCommGroup
⊢ ∀ ⦃x y : α →ᵇ β⦄, |x| ≤ |y| → ‖x‖ ≤ ‖y‖
[PROOFSTEP]
intro f g h
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝¹ : Lattice (α →ᵇ β) := lattice
src✝ : SeminormedAddCommGroup (α →ᵇ β) := seminormedAddCommGroup
f g : α →ᵇ β
h : |f| ≤ |g|
⊢ ‖f‖ ≤ ‖g‖
[PROOFSTEP]
have i1 : ∀ t, ‖f t‖ ≤ ‖g t‖ := fun t => HasSolidNorm.solid (h t)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝¹ : Lattice (α →ᵇ β) := lattice
src✝ : SeminormedAddCommGroup (α →ᵇ β) := seminormedAddCommGroup
f g : α →ᵇ β
h : |f| ≤ |g|
i1 : ∀ (t : α), ‖↑f t‖ ≤ ‖↑g t‖
⊢ ‖f‖ ≤ ‖g‖
[PROOFSTEP]
rw [norm_le (norm_nonneg _)]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝¹ : Lattice (α →ᵇ β) := lattice
src✝ : SeminormedAddCommGroup (α →ᵇ β) := seminormedAddCommGroup
f g : α →ᵇ β
h : |f| ≤ |g|
i1 : ∀ (t : α), ‖↑f t‖ ≤ ‖↑g t‖
⊢ ∀ (x : α), ‖↑f x‖ ≤ ‖g‖
[PROOFSTEP]
exact fun t =>
  (i1 t).trans
    (norm_coe_le_norm g t)
      -- Porting note: Added a proof for `eq_of_dist_eq_zero`
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝¹ : Lattice (α →ᵇ β) := lattice
src✝ : SeminormedAddCommGroup (α →ᵇ β) := seminormedAddCommGroup
⊢ ∀ (a b : α →ᵇ β), a ≤ b → ∀ (c : α →ᵇ β), c + a ≤ c + b
[PROOFSTEP]
intro f g h₁ h t
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝¹ : Lattice (α →ᵇ β) := lattice
src✝ : SeminormedAddCommGroup (α →ᵇ β) := seminormedAddCommGroup
f g : α →ᵇ β
h₁ : f ≤ g
h : α →ᵇ β
t : α
⊢ (fun f => f.toFun) (h + f) t ≤ (fun f => f.toFun) (h + g) t
[PROOFSTEP]
simp only [coe_to_continuous_fun, Pi.add_apply, add_le_add_iff_left, coe_add, ContinuousMap.toFun_eq_coe]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup β
src✝¹ : Lattice (α →ᵇ β) := lattice
src✝ : SeminormedAddCommGroup (α →ᵇ β) := seminormedAddCommGroup
f g : α →ᵇ β
h₁ : f ≤ g
h : α →ᵇ β
t : α
⊢ ↑f t ≤ ↑g t
[PROOFSTEP]
exact h₁ _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
⊢ ↑f = toReal ∘ ↑(nnrealPart f) - toReal ∘ ↑(nnrealPart (-f))
[PROOFSTEP]
funext x
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ ↑f x = (toReal ∘ ↑(nnrealPart f) - toReal ∘ ↑(nnrealPart (-f))) x
[PROOFSTEP]
dsimp
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ ↑f x = max (↑f x) 0 - max (-↑f x) 0
[PROOFSTEP]
simp only [max_zero_sub_max_neg_zero_eq_self]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
⊢ abs ∘ ↑f = toReal ∘ ↑(nnrealPart f) + toReal ∘ ↑(nnrealPart (-f))
[PROOFSTEP]
funext x
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (abs ∘ ↑f) x = (toReal ∘ ↑(nnrealPart f) + toReal ∘ ↑(nnrealPart (-f))) x
[PROOFSTEP]
dsimp
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ |↑f x| = max (↑f x) 0 + max (-↑f x) 0
[PROOFSTEP]
simp only [max_zero_add_max_neg_zero_eq_abs_self]
