Auxiliary lemmas

Small helper lemmas about CauSeq suprema/infima and about Cauchy sequences converging to a real number, used in the construction of computable reals.

theorem abs_ite_le {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (x : α) : |x| = if 0 ≤ x then x else -x

theorem CauSeq.sup_equiv_of_equivs {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : CauSeq α abs} (ha : a ≈ c) (hb : b ≈ c) : a ⊔ b ≈ c

theorem CauSeq.equiv_sup_of_equivs {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : CauSeq α abs} (ha : c ≈ a) (hb : c ≈ b) : c ≈ a ⊔ b

theorem CauSeq.inf_equiv_of_equivs {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : CauSeq α abs} (ha : a ≈ c) (hb : b ≈ c) : a ⊓ b ≈ c

def CauSeq.drop {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : CauSeq α abs) (n : ℕ) : CauSeq α abs

Dropping the first n terms of a Cauchy sequence to get a new sequence.

Equations

• a.drop n = ⟨fun (k : ℕ) => ↑a (n + k), ⋯⟩

theorem CauSeq.drop_equiv_self {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : CauSeq α abs) (n : ℕ) : a.drop n ≈ a

Dropping elements from a Cauchy sequence gives an equivalent one.

theorem Real.exists_CauSeq (x : ℝ) : ∃ (s : CauSeq ℚ abs), mk s = x

Every real number has some Caucy sequence converging to it.

theorem cauchy_real_mk (x : CauSeq ℚ abs) (ε : ℝ) : ε > 0 → ∃ (i : ℕ), ∀ j ≥ i, |↑(↑x j) - Real.mk x| < ε