[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f g : α →C₀ β
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✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
g : α →C₀ β
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
zero_at_infty'✝ : Tendsto (ContinuousMap.mk toFun✝).toFun (cocompact α) (𝓝 0)
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, zero_at_infty' := zero_at_infty'✝ } =
    (fun f => f.toFun) g
⊢ { toContinuousMap := ContinuousMap.mk toFun✝, zero_at_infty' := zero_at_infty'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
zero_at_infty'✝¹ : Tendsto (ContinuousMap.mk toFun✝¹).toFun (cocompact α) (𝓝 0)
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
zero_at_infty'✝ : Tendsto (ContinuousMap.mk toFun✝).toFun (cocompact α) (𝓝 0)
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, zero_at_infty' := zero_at_infty'✝ }
⊢ { toContinuousMap := ContinuousMap.mk toFun✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    { toContinuousMap := ContinuousMap.mk toFun✝, zero_at_infty' := zero_at_infty'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ↑f
⊢ Continuous f'
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ↑f
⊢ Continuous ↑f
[PROOFSTEP]
exact f.continuous_toFun
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ↑f
⊢ Tendsto (ContinuousMap.mk f').toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simp_rw [h]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ↑f
⊢ Tendsto (↑f) (cocompact α) (𝓝 0)
[PROOFSTEP]
exact f.zero_at_infty'
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : C(α, β)
⊢ Tendsto (ContinuousMap.mk ↑f).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : C(α, β)
⊢ (fun f => ↑f)
      ((fun f => { toContinuousMap := ContinuousMap.mk ↑f, zero_at_infty' := (_ : Tendsto (↑f) (cocompact α) (𝓝 0)) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : C(α, β)
a✝ : α
⊢ ↑((fun f => ↑f)
          ((fun f =>
              { toContinuousMap := ContinuousMap.mk ↑f, zero_at_infty' := (_ : Tendsto (↑f) (cocompact α) (𝓝 0)) })
            f))
      a✝ =
    ↑f a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : α →C₀ β
⊢ (fun f => { toContinuousMap := ContinuousMap.mk ↑f, zero_at_infty' := (_ : Tendsto (↑f) (cocompact α) (𝓝 0)) })
      ((fun f => ↑f) f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : α →C₀ β
x✝ : α
⊢ ↑((fun f => { toContinuousMap := ContinuousMap.mk ↑f, zero_at_infty' := (_ : Tendsto (↑f) (cocompact α) (𝓝 0)) })
          ((fun f => ↑f) f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Zero β
inst✝² : ZeroAtInftyContinuousMapClass F α β
G : Type u_2
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
⊢ ∀ (f : G), Tendsto (↑f) (cocompact α) (𝓝 0)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : MulZeroClass β
inst✝ : ContinuousMul β
f g : α →C₀ β
⊢ Tendsto (↑f * ↑g).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa only [mul_zero] using (zero_at_infty f).mul (zero_at_infty g)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddZeroClass β
inst✝ : ContinuousAdd β
f g : α →C₀ β
⊢ Tendsto (↑f + ↑g).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa only [add_zero] using (zero_at_infty f).add (zero_at_infty g)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
f g : α →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✝² : TopologicalSpace β
x : α
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
f g : α →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✝² : TopologicalSpace β
x : α
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
f✝ g : α →C₀ β
n : ℕ
f : α →C₀ β
⊢ Tendsto (n • ↑f).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa [coe_nsmulRec] using zero_at_infty (nsmulRec n f)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f✝ g f : α →C₀ β
⊢ Tendsto (-↑f).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa only [neg_zero] using (zero_at_infty f).neg
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f✝ g✝ f g : α →C₀ β
⊢ Tendsto (↑f - ↑g).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa only [sub_zero] using (zero_at_infty f).sub (zero_at_infty g)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f g : α →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✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f g : α →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✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f✝ g : α →C₀ β
n : ℤ
f : α →C₀ β
⊢ Tendsto (ContinuousMap.mk (n • ↑f)).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa using zero_at_infty (zsmulRec n f)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
x : α
inst✝³ : Zero β
R : Type u_2
inst✝² : Zero R
inst✝¹ : SMulWithZero R β
inst✝ : ContinuousConstSMul R β
r : R
f : α →C₀ β
⊢ Tendsto (ContinuousMap.mk (r • ↑f)).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa [smul_zero] using (zero_at_infty f).const_smul r
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : IsScalarTower R β β
r : R
f g : α →C₀ β
⊢ (r • f) • g = r • f • g
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : IsScalarTower R β β
r : R
f g : α →C₀ β
x✝ : α
⊢ ↑((r • f) • g) x✝ = ↑(r • f • g) x✝
[PROOFSTEP]
simp only [smul_eq_mul, coe_mul, coe_smul, Pi.mul_apply, Pi.smul_apply]
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : IsScalarTower R β β
r : R
f g : α →C₀ β
x✝ : α
⊢ r • ↑f x✝ * ↑g x✝ = r • (↑f x✝ * ↑g x✝)
[PROOFSTEP]
rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C₀ β
⊢ r • f • g = f • r • g
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C₀ β
x✝ : α
⊢ ↑(r • f • g) x✝ = ↑(f • r • g) x✝
[PROOFSTEP]
simp only [smul_eq_mul, coe_smul, coe_mul, Pi.smul_apply, Pi.mul_apply]
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C₀ β
x✝ : α
⊢ r • (↑f x✝ * ↑g x✝) = ↑f x✝ * r • ↑g x✝
[PROOFSTEP]
rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
⊢ ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C
[PROOFSTEP]
obtain ⟨K : Set α, hK₁, hK₂⟩ :=
  mem_cocompact.mp (tendsto_def.mp (zero_at_infty (f : F)) _ (closedBall_mem_nhds (0 : β) zero_lt_one))
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
⊢ ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C
[PROOFSTEP]
obtain ⟨C, hC⟩ := (hK₁.image (map_continuous f)).bounded.subset_ball (0 : β)
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
⊢ ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C
[PROOFSTEP]
refine' ⟨max C 1 + max C 1, fun x y => _⟩
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x y : α
⊢ dist (↑f x) (↑f y) ≤ max C 1 + max C 1
[PROOFSTEP]
have : ∀ x, f x ∈ closedBall (0 : β) (max C 1) := by
  intro x
  by_cases hx : x ∈ K
  · exact (mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)
  · exact (mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x y : α
⊢ ∀ (x : α), ↑f x ∈ closedBall 0 (max C 1)
[PROOFSTEP]
intro x
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x✝ y x : α
⊢ ↑f x ∈ closedBall 0 (max C 1)
[PROOFSTEP]
by_cases hx : x ∈ K
[GOAL]
case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x✝ y x : α
hx : x ∈ K
⊢ ↑f x ∈ closedBall 0 (max C 1)
[PROOFSTEP]
exact (mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)
[GOAL]
case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x✝ y x : α
hx : ¬x ∈ K
⊢ ↑f x ∈ closedBall 0 (max C 1)
[PROOFSTEP]
exact (mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x y : α
this : ∀ (x : α), ↑f x ∈ closedBall 0 (max C 1)
⊢ dist (↑f x) (↑f y) ≤ max C 1 + max C 1
[PROOFSTEP]
exact (dist_triangle (f x) 0 (f y)).trans (add_le_add (mem_closedBall.mp <| this x) (mem_closedBall'.mp <| this y))
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f g : α →C₀ β
h : toBcf f = toBcf g
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f g : α →C₀ β
h : toBcf f = toBcf g
x : α
⊢ ↑f x = ↑g x
[PROOFSTEP]
simpa only using FunLike.congr_fun h x
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F✝ α β
C : ℝ
f✝ g : α →C₀ β
ι : Type u_2
F : ι → α →C₀ β
f : α →C₀ β
l : Filter ι
⊢ Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i => ↑(F i)) (↑f) l
[PROOFSTEP]
simpa only [Metric.tendsto_nhds] using
  @BoundedContinuousFunction.tendsto_iff_tendstoUniformly _ _ _ _ _ (fun i => (F i).toBcf) f.toBcf l
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f g : α →C₀ β
⊢ Isometry toBcf
[PROOFSTEP]
tauto
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f g : α →C₀ β
⊢ IsClosed (range toBcf)
[PROOFSTEP]
refine' isClosed_iff_clusterPt.mpr fun f hf => _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g : α →C₀ β
f : α →ᵇ β
hf : ClusterPt f (𝓟 (range toBcf))
⊢ f ∈ range toBcf
[PROOFSTEP]
rw [clusterPt_principal_iff] at hf 
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
⊢ f ∈ range toBcf
[PROOFSTEP]
have : Tendsto f (cocompact α) (𝓝 0) :=
  by
  refine' Metric.tendsto_nhds.mpr fun ε hε => _
  obtain ⟨_, hg, g, rfl⟩ := hf (ball f (ε / 2)) (ball_mem_nhds f <| half_pos hε)
  refine' (Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp (eventually_of_forall fun x hx => _)
  calc
    dist (f x) 0 ≤ dist (g.toBcf x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
    _ < dist g.toBcf f + ε / 2 := (add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx)
    _ < ε := by simpa [add_halves ε] using add_lt_add_right (mem_ball.1 hg) (ε / 2)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
⊢ Tendsto (↑f) (cocompact α) (𝓝 0)
[PROOFSTEP]
refine' Metric.tendsto_nhds.mpr fun ε hε => _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : α) in cocompact α, dist (↑f x) 0 < ε
[PROOFSTEP]
obtain ⟨_, hg, g, rfl⟩ := hf (ball f (ε / 2)) (ball_mem_nhds f <| half_pos hε)
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g✝ : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : toBcf g ∈ ball f (ε / 2)
⊢ ∀ᶠ (x : α) in cocompact α, dist (↑f x) 0 < ε
[PROOFSTEP]
refine' (Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp (eventually_of_forall fun x hx => _)
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g✝ : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : toBcf g ∈ ball f (ε / 2)
x : α
hx : dist (↑g x) 0 < ε / 2
⊢ dist (↑f x) 0 < ε
[PROOFSTEP]
calc
  dist (f x) 0 ≤ dist (g.toBcf x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
  _ < dist g.toBcf f + ε / 2 := (add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx)
  _ < ε := by simpa [add_halves ε] using add_lt_add_right (mem_ball.1 hg) (ε / 2)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g✝ : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : toBcf g ∈ ball f (ε / 2)
x : α
hx : dist (↑g x) 0 < ε / 2
⊢ dist (toBcf g) f + ε / 2 < ε
[PROOFSTEP]
simpa [add_halves ε] using add_lt_add_right (mem_ball.1 hg) (ε / 2)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
this : Tendsto (↑f) (cocompact α) (𝓝 0)
⊢ f ∈ range toBcf
[PROOFSTEP]
exact ⟨⟨f.toContinuousMap, this⟩, rfl⟩
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : AddMonoid β
inst✝¹ : StarAddMonoid β
inst✝ : ContinuousStar β
f : α →C₀ β
⊢ Tendsto (ContinuousMap.mk fun x => star (↑f x)).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa only [star_zero] using (continuous_star.tendsto (0 : β)).comp (zero_at_infty f)
