theorem Chapter6.Sequence.isCauchy_iff_isCauSeq (a : ℕ → ℝ) : (↑a).IsCauchy ↔ IsCauSeq _root_.abs a

Identification with the Cauchy sequence support in Mathlib/Algebra/Order/CauSeq/Basic

theorem Chapter6.Sequence.Cauchy_iff_CauchySeq (a : ℕ → ℝ) : (↑a).IsCauchy ↔ CauchySeq a

Identification with the Cauchy sequence support in Mathlib/Topology/UniformSpace/Cauchy

theorem Chapter6.Sequence.tendsto_iff_Tendsto (a : ℕ → ℝ) (L : ℝ) : (↑a).TendsTo L ↔ Filter.Tendsto a Filter.atTop (nhds L)

Identification with Filter.Tendsto

theorem Chapter6.Sequence.tendsto_iff_Tendsto' (a : Sequence) (L : ℝ) : a.TendsTo L ↔ Filter.Tendsto a.seq Filter.atTop (nhds L)

theorem Chapter6.Sequence.converges_iff_Tendsto (a : ℕ → ℝ) : (↑a).Convergent ↔ ∃ (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L)

theorem Chapter6.Sequence.converges_iff_Tendsto' (a : Sequence) : a.Convergent ↔ ∃ (L : ℝ), Filter.Tendsto a.seq Filter.atTop (nhds L)

instance inst_real_complete : CauSeq.IsComplete ℝ norm

A technicality: CauSeq.IsComplete ℝ was established for _root_.abs but not for norm.

theorem Chapter6.Sequence.lim_eq_CauSeq_lim (a : ℕ → ℝ) (ha : (↑a).IsCauchy) : lim ↑a = CauSeq.lim ⟨a, ⋯⟩

Identification with CauSeq.lim

theorem Chapter6.Sequence.lim_eq_limUnder (a : ℕ → ℝ) (ha : (↑a).Convergent) : lim ↑a = Filter.atTop.limUnder a

Identification with limUnder

theorem Chapter6.Sequence.isBounded_iff_isBounded_range (a : ℕ → ℝ) : (↑a).IsBounded ↔ Bornology.IsBounded (Set.range a)

Identification with Bornology.IsBounded

theorem Chapter6.Sequence.sup_eq_sSup (a : ℕ → ℝ) : (↑a).sup = sSup (Set.range fun (n : ℕ) => ↑(a n))

theorem Chapter6.Sequence.inf_eq_sInf (a : ℕ → ℝ) : (↑a).inf = sInf (Set.range fun (n : ℕ) => ↑(a n))

theorem Chapter6.Sequence.bddAbove_iff (a : ℕ → ℝ) : (↑a).BddAbove ↔ _root_.BddAbove (Set.range a)

theorem Chapter6.Sequence.bddBelow_iff (a : ℕ → ℝ) : (↑a).BddBelow ↔ _root_.BddBelow (Set.range a)

theorem Chapter6.Sequence.Monotone_iff (a : ℕ → ℝ) : (↑a).IsMonotone ↔ Monotone a

theorem Chapter6.Sequence.Antitone_iff (a : ℕ → ℝ) : (↑a).IsAntitone ↔ Antitone a

theorem Chapter6.Sequence.limit_point_iff (a : ℕ → ℝ) (L : ℝ) : (↑a).LimitPoint L ↔ MapClusterPt L Filter.atTop a

Identification with MapClusterPt

theorem Chapter6.Sequence.limsup_eq (a : ℕ → ℝ) : (↑a).limsup = Filter.limsup (fun (n : ℕ) => ↑(a n)) Filter.atTop

Identification with Filter.limsup

theorem Chapter6.Sequence.liminf_eq (a : ℕ → ℝ) : (↑a).liminf = Filter.liminf (fun (n : ℕ) => ↑(a n)) Filter.atTop

Identification with Filter.liminf

theorem Chapter6.Real.rpow_eq_rpow {x : ℝ} (hx : x > 0) (α : ℝ) : rpow x α = x ^ α

Identification of Chapter6.Real.rpow and Mathlib exponentiation