cauchySeq_comp_iff — Mathlib

English

For bijective f: ℕ → ℕ, CauchySeq(u ∘ f) ↔ CauchySeq u.

Русский

Для биективного f: ℕ → ℕ, CauchySeq(u ∘ f) эквивалентно CauchySeq u.

LaTeX

$$$\\text{CauchySeq}(u\\circ f) \\iff \\text{CauchySeq}(u)\\quad( f \\text{ bijective}).$$$

Lean4

theorem cauchySeq_comp_iff {f : ℕ → ℕ} (hf : Bijective f) (u : ℕ → α) : CauchySeq (u ∘ f) ↔ CauchySeq u :=
  by
  refine ⟨fun H => ?_, fun H => H.comp_injective hf.injective⟩
  lift f to ℕ ≃ ℕ using hf
  simpa only [Function.comp_def, f.apply_symm_apply] using H.comp_injective f.symm.injective

Похожие утверждения