α : Type u
β : Type v
inst✝ : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
H : CauchySeq (u ∘ f)
⊢ CauchySeq u
α : Type u
β : Type v
inst✝ : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
⊢ CauchySeq (u ∘ f) ↔ CauchySeq u
refine' ⟨fun H => _, fun H => H.comp_injective hf.injective⟩
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
u : ℕ → α
f : ℕ ≃ ℕ
H : CauchySeq (u ∘ ↑f)
⊢ CauchySeq u
α : Type u
β : Type v
inst✝ : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
H : CauchySeq (u ∘ f)
⊢ CauchySeq u
lift f to ℕ ≃ ℕ using hf