# mathlib3documentation

data.real.cau_seq

# Cauchy sequences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A basic theory of Cauchy sequences, used in the construction of the reals and p-adic numbers. Where applicable, lemmas that will be reused in other contexts have been stated in extra generality.

There are other "versions" of Cauchyness in the library, in particular Cauchy filters in topology. This is a concrete implementation that is useful for simplicity and computability reasons.

## Important definitions #

• `is_cau_seq`: a predicate that says `f : ℕ → β` is Cauchy.
• `cau_seq`: the type of Cauchy sequences valued in type `β` with respect to an absolute value function `abv`.

## Tags #

sequence, cauchy, abs val, absolute value

theorem exists_forall_ge_and {α : Type u_1} [linear_order α] {P Q : α Prop} :
( (i : α), (j : α), j i P j) ( (i : α), (j : α), j i Q j) ( (i : α), (j : α), j i P j Q j)
theorem rat_add_continuous_lemma {α : Type u_2} {β : Type u_3} [ring β] (abv : β α) [is_absolute_value abv] {ε : α} (ε0 : 0 < ε) :
(δ : α) (H : δ > 0), {a₁ a₂ b₁ b₂ : β}, abv (a₁ - b₁) < δ abv (a₂ - b₂) < δ abv (a₁ + a₂ - (b₁ + b₂)) < ε
theorem rat_mul_continuous_lemma {α : Type u_2} {β : Type u_3} [ring β] (abv : β α) [is_absolute_value abv] {ε K₁ K₂ : α} (ε0 : 0 < ε) :
(δ : α) (H : δ > 0), {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ abv b₂ < K₂ abv (a₁ - b₁) < δ abv (a₂ - b₂) < δ abv (a₁ * a₂ - b₁ * b₂) < ε
theorem rat_inv_continuous_lemma {α : Type u_2} {β : Type u_1} (abv : β α) [is_absolute_value abv] {ε K : α} (ε0 : 0 < ε) (K0 : 0 < K) :
(δ : α) (H : δ > 0), {a b : β}, K abv a K abv b abv (a - b) < δ abv (a⁻¹ - b⁻¹) < ε
def is_cau_seq {α : Type u_1} {β : Type u_2} [ring β] (abv : β α) (f : β) :
Prop

A sequence is Cauchy if the distance between its entries tends to zero.

Equations
@[nolint]
theorem is_cau_seq.cauchy₂ {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f : β} (hf : is_cau_seq abv f) {ε : α} (ε0 : 0 < ε) :
(i : ), (j : ), j i (k : ), k i abv (f j - f k) < ε
theorem is_cau_seq.cauchy₃ {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f : β} (hf : is_cau_seq abv f) {ε : α} (ε0 : 0 < ε) :
(i : ), (j : ), j i (k : ), k j abv (f k - f j) < ε
theorem is_cau_seq.add {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f g : β} (hf : is_cau_seq abv f) (hg : is_cau_seq abv g) :
is_cau_seq abv (f + g)
def cau_seq {α : Type u_1} (β : Type u_2) [ring β] (abv : β α) :
Type u_2

`cau_seq β abv` is the type of `β`-valued Cauchy sequences, with respect to the absolute value function `abv`.

Equations
Instances for `cau_seq`
@[protected, instance]
def cau_seq.has_coe_to_fun {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} :
has_coe_to_fun (cau_seq β abv) (λ (_x : abv), β)
Equations
@[simp]
theorem cau_seq.mk_to_fun {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} (f : β) (hf : is_cau_seq abv f) :
f, hf⟩ = f
theorem cau_seq.ext {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} {f g : abv} (h : (i : ), f i = g i) :
f = g
theorem cau_seq.is_cau {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} (f : abv) :
theorem cau_seq.cauchy {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} (f : abv) {ε : α} :
0 < ε ( (i : ), (j : ), j i abv (f j - f i) < ε)
def cau_seq.of_eq {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} (f : abv) (g : β) (e : (i : ), f i = g i) :
abv

Given a Cauchy sequence `f`, create a Cauchy sequence from a sequence `g` with the same values as `f`.

Equations
@[nolint]
theorem cau_seq.cauchy₂ {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) {ε : α} :
0 < ε ( (i : ), (j : ), j i (k : ), k i abv (f j - f k) < ε)
theorem cau_seq.cauchy₃ {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) {ε : α} :
0 < ε ( (i : ), (j : ), j i (k : ), k j abv (f k - f j) < ε)
theorem cau_seq.bounded {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) :
(r : α), (i : ), abv (f i) < r
theorem cau_seq.bounded' {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) (x : α) :
(r : α) (H : r > x), (i : ), abv (f i) < r
@[protected, instance]
def cau_seq.has_add {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
has_add (cau_seq β abv)
Equations
@[simp, norm_cast]
theorem cau_seq.coe_add {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f g : abv) :
(f + g) = f + g
@[simp, norm_cast]
theorem cau_seq.add_apply {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f g : abv) (i : ) :
(f + g) i = f i + g i
def cau_seq.const {α : Type u_2} {β : Type u_3} [ring β] (abv : β α) [is_absolute_value abv] (x : β) :
abv

The constant Cauchy sequence.

Equations
@[simp, norm_cast]
theorem cau_seq.coe_const {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (x : β) :
@[simp, norm_cast]
theorem cau_seq.const_apply {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (x : β) (i : ) :
(cau_seq.const abv x) i = x
theorem cau_seq.const_inj {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {x y : β} :
x = y x = y
@[protected, instance]
def cau_seq.has_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
has_zero (cau_seq β abv)
Equations
@[protected, instance]
def cau_seq.has_one {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
has_one (cau_seq β abv)
Equations
@[protected, instance]
def cau_seq.inhabited {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[simp, norm_cast]
theorem cau_seq.coe_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
0 = 0
@[simp, norm_cast]
theorem cau_seq.coe_one {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
1 = 1
@[simp, norm_cast]
theorem cau_seq.zero_apply {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (i : ) :
0 i = 0
@[simp, norm_cast]
theorem cau_seq.one_apply {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (i : ) :
1 i = 1
@[simp]
theorem cau_seq.const_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
0 = 0
@[simp]
theorem cau_seq.const_one {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
1 = 1
theorem cau_seq.const_add {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (x y : β) :
(x + y) = x + y
@[protected, instance]
def cau_seq.has_mul {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
has_mul (cau_seq β abv)
Equations
@[simp, norm_cast]
theorem cau_seq.coe_mul {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f g : abv) :
(f * g) = f * g
@[simp, norm_cast]
theorem cau_seq.mul_apply {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f g : abv) (i : ) :
(f * g) i = f i * g i
theorem cau_seq.const_mul {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (x y : β) :
(x * y) = x * y
@[protected, instance]
def cau_seq.has_neg {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
has_neg (cau_seq β abv)
Equations
@[simp, norm_cast]
theorem cau_seq.coe_neg {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) :
@[simp, norm_cast]
theorem cau_seq.neg_apply {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) (i : ) :
(-f) i = -f i
theorem cau_seq.const_neg {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (x : β) :
(-x) = - x
@[protected, instance]
def cau_seq.has_sub {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
has_sub (cau_seq β abv)
Equations
@[simp, norm_cast]
theorem cau_seq.coe_sub {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f g : abv) :
(f - g) = f - g
@[simp, norm_cast]
theorem cau_seq.sub_apply {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f g : abv) (i : ) :
(f - g) i = f i - g i
theorem cau_seq.const_sub {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (x y : β) :
(x - y) = x - y
@[protected, instance]
def cau_seq.has_smul {G : Type u_1} {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] [ β] [ β] :
(cau_seq β abv)
Equations
@[simp, norm_cast]
theorem cau_seq.coe_smul {G : Type u_1} {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] [ β] [ β] (a : G) (f : abv) :
(a f) = a f
@[simp, norm_cast]
theorem cau_seq.smul_apply {G : Type u_1} {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] [ β] [ β] (a : G) (f : abv) (i : ) :
(a f) i = a f i
theorem cau_seq.const_smul {G : Type u_1} {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] [ β] [ β] (a : G) (x : β) :
(a x) = a x
@[protected, instance]
def cau_seq.is_scalar_tower {G : Type u_1} {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] [ β] [ β] :
(cau_seq β abv) (cau_seq β abv)
@[protected, instance]
def cau_seq.add_group {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[protected, instance]
def cau_seq.add_group_with_one {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[protected, instance]
def cau_seq.nat.has_pow {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[simp, norm_cast]
theorem cau_seq.coe_pow {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) (n : ) :
(f ^ n) = f ^ n
@[simp, norm_cast]
theorem cau_seq.pow_apply {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) (n i : ) :
(f ^ n) i = f i ^ n
theorem cau_seq.const_pow {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (x : β) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
def cau_seq.ring {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
ring (cau_seq β abv)
Equations
@[protected, instance]
def cau_seq.comm_ring {α : Type u_2} {β : Type u_1} [comm_ring β] {abv : β α} [is_absolute_value abv] :
Equations
def cau_seq.lim_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} (f : abv) :
Prop

`lim_zero f` holds when `f` approaches 0.

Equations
theorem cau_seq.add_lim_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f g : abv} (hf : f.lim_zero) (hg : g.lim_zero) :
(f + g).lim_zero
theorem cau_seq.mul_lim_zero_right {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) {g : abv} (hg : g.lim_zero) :
(f * g).lim_zero
theorem cau_seq.mul_lim_zero_left {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f : abv} (g : abv) (hg : f.lim_zero) :
(f * g).lim_zero
theorem cau_seq.neg_lim_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f : abv} (hf : f.lim_zero) :
theorem cau_seq.sub_lim_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f g : abv} (hf : f.lim_zero) (hg : g.lim_zero) :
(f - g).lim_zero
theorem cau_seq.lim_zero_sub_rev {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f g : abv} (hfg : (f - g).lim_zero) :
(g - f).lim_zero
theorem cau_seq.zero_lim_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
theorem cau_seq.const_lim_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {x : β} :
@[protected, instance]
def cau_seq.equiv {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] :
setoid (cau_seq β abv)
Equations
theorem cau_seq.add_equiv_add {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f1 f2 g1 g2 : abv} (hf : f1 f2) (hg : g1 g2) :
f1 + g1 f2 + g2
theorem cau_seq.neg_equiv_neg {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f g : abv} (hf : f g) :
-f -g
theorem cau_seq.sub_equiv_sub {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f1 f2 g1 g2 : abv} (hf : f1 f2) (hg : g1 g2) :
f1 - g1 f2 - g2
theorem cau_seq.equiv_def₃ {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f g : abv} (h : f g) {ε : α} (ε0 : 0 < ε) :
(i : ), (j : ), j i (k : ), k j abv (f k - g j) < ε
theorem cau_seq.lim_zero_congr {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f g : abv} (h : f g) :
theorem cau_seq.abv_pos_of_not_lim_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f : abv} (hf : ¬f.lim_zero) :
(K : α) (H : K > 0) (i : ), (j : ), j i K abv (f j)
theorem cau_seq.of_near {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (f : β) (g : abv) (h : (ε : α), ε > 0 ( (i : ), (j : ), j i abv (f j - g j) < ε)) :
theorem cau_seq.not_lim_zero_of_not_congr_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f : abv} (hf : ¬f 0) :
theorem cau_seq.mul_equiv_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (g : abv) {f : abv} (hf : f 0) :
g * f 0
theorem cau_seq.mul_equiv_zero' {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] (g : abv) {f : abv} (hf : f 0) :
f * g 0
theorem cau_seq.mul_not_equiv_zero {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f g : abv} (hf : ¬f 0) (hg : ¬g 0) :
¬f * g 0
theorem cau_seq.const_equiv {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {x y : β} :
x y x = y
theorem cau_seq.mul_equiv_mul {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f1 f2 g1 g2 : abv} (hf : f1 f2) (hg : g1 g2) :
f1 * g1 f2 * g2
theorem cau_seq.smul_equiv_smul {G : Type u_1} {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] [ β] [ β] {f1 f2 : abv} (c : G) (hf : f1 f2) :
c f1 c f2
theorem cau_seq.pow_equiv_pow {α : Type u_2} {β : Type u_3} [ring β] {abv : β α} [is_absolute_value abv] {f1 f2 : abv} (hf : f1 f2) (n : ) :
f1 ^ n f2 ^ n
theorem cau_seq.one_not_equiv_zero {α : Type u_2} {β : Type u_3} [ring β] [is_domain β] (abv : β α) [is_absolute_value abv] :
¬ 1 0
theorem cau_seq.inv_aux {α : Type u_2} {β : Type u_3} {abv : β α} [is_absolute_value abv] {f : abv} (hf : ¬f.lim_zero) (ε : α) (H : ε > 0) :
(i : ), (j : ), j i abv ((f j)⁻¹ - (f i)⁻¹) < ε
def cau_seq.inv {α : Type u_2} {β : Type u_3} {abv : β α} [is_absolute_value abv] (f : abv) (hf : ¬f.lim_zero) :
abv

Given a Cauchy sequence `f` with nonzero limit, create a Cauchy sequence with values equal to the inverses of the values of `f`.

Equations
@[simp, norm_cast]
theorem cau_seq.coe_inv {α : Type u_2} {β : Type u_3} {abv : β α} [is_absolute_value abv] {f : abv} (hf : ¬f.lim_zero) :
(f.inv hf) = (f)⁻¹
@[simp, norm_cast]
theorem cau_seq.inv_apply {α : Type u_2} {β : Type u_3} {abv : β α} [is_absolute_value abv] {f : abv} (hf : ¬f.lim_zero) (i : ) :
(f.inv hf) i = (f i)⁻¹
theorem cau_seq.inv_mul_cancel {α : Type u_2} {β : Type u_3} {abv : β α} [is_absolute_value abv] {f : abv} (hf : ¬f.lim_zero) :
f.inv hf * f 1
theorem cau_seq.mul_inv_cancel {α : Type u_2} {β : Type u_3} {abv : β α} [is_absolute_value abv] {f : abv} (hf : ¬f.lim_zero) :
f * f.inv hf 1
theorem cau_seq.const_inv {α : Type u_2} {β : Type u_3} {abv : β α} [is_absolute_value abv] {x : β} (hx : x 0) :
x⁻¹ = (cau_seq.const abv x).inv _
def cau_seq.pos {α : Type u_2} (f : has_abs.abs) :
Prop

The entries of a positive Cauchy sequence eventually have a positive lower bound.

Equations
theorem cau_seq.const_pos {α : Type u_2} {x : α} :
0 < x
theorem cau_seq.add_pos {α : Type u_2} {f g : has_abs.abs} :
f.pos g.pos (f + g).pos
theorem cau_seq.pos_add_lim_zero {α : Type u_2} {f g : has_abs.abs} :
f.pos g.lim_zero (f + g).pos
@[protected]
theorem cau_seq.mul_pos {α : Type u_2} {f g : has_abs.abs} :
f.pos g.pos (f * g).pos
theorem cau_seq.trichotomy {α : Type u_2} (f : has_abs.abs) :
@[protected, instance]
def cau_seq.has_lt {α : Type u_2}  :
Equations
@[protected, instance]
def cau_seq.has_le {α : Type u_2}  :
Equations
theorem cau_seq.lt_of_lt_of_eq {α : Type u_2} {f g h : has_abs.abs} (fg : f < g) (gh : g h) :
f < h
theorem cau_seq.lt_of_eq_of_lt {α : Type u_2} {f g h : has_abs.abs} (fg : f g) (gh : g < h) :
f < h
theorem cau_seq.lt_trans {α : Type u_2} {f g h : has_abs.abs} (fg : f < g) (gh : g < h) :
f < h
theorem cau_seq.lt_irrefl {α : Type u_2} {f : has_abs.abs} :
¬f < f
theorem cau_seq.le_of_eq_of_le {α : Type u_2} {f g h : has_abs.abs} (hfg : f g) (hgh : g h) :
f h
theorem cau_seq.le_of_le_of_eq {α : Type u_2} {f g h : has_abs.abs} (hfg : f g) (hgh : g h) :
f h
@[protected, instance]
def cau_seq.preorder {α : Type u_2}  :
Equations
theorem cau_seq.le_antisymm {α : Type u_2} {f g : has_abs.abs} (fg : f g) (gf : g f) :
f g
theorem cau_seq.lt_total {α : Type u_2} (f g : has_abs.abs) :
f < g f g g < f
theorem cau_seq.le_total {α : Type u_2} (f g : has_abs.abs) :
f g g f
theorem cau_seq.const_lt {α : Type u_2} {x y : α} :
theorem cau_seq.const_le {α : Type u_2} {x y : α} :
theorem cau_seq.le_of_exists {α : Type u_2} {f g : has_abs.abs} (h : (i : ), (j : ), j i f j g j) :
f g
theorem cau_seq.exists_gt {α : Type u_2} (f : has_abs.abs) :
(a : α),
theorem cau_seq.exists_lt {α : Type u_2} (f : has_abs.abs) :
(a : α),
theorem rat_sup_continuous_lemma {α : Type u_2} {ε a₁ a₂ b₁ b₂ : α} :
|a₁ - b₁| < ε |a₂ - b₂| < ε |a₁ a₂ - b₁ b₂| < ε
theorem rat_inf_continuous_lemma {α : Type u_2} {ε a₁ a₂ b₁ b₂ : α} :
|a₁ - b₁| < ε |a₂ - b₂| < ε |a₁ a₂ - b₁ b₂| < ε
@[protected, instance]
def cau_seq.has_sup {α : Type u_2}  :
Equations
@[protected, instance]
def cau_seq.has_inf {α : Type u_2}  :
Equations
@[simp, norm_cast]
theorem cau_seq.coe_sup {α : Type u_2} (f g : has_abs.abs) :
(f g) = f g
@[simp, norm_cast]
theorem cau_seq.coe_inf {α : Type u_2} (f g : has_abs.abs) :
(f g) = f g
theorem cau_seq.sup_lim_zero {α : Type u_2} {f g : has_abs.abs} (hf : f.lim_zero) (hg : g.lim_zero) :
theorem cau_seq.inf_lim_zero {α : Type u_2} {f g : has_abs.abs} (hf : f.lim_zero) (hg : g.lim_zero) :
theorem cau_seq.sup_equiv_sup {α : Type u_2} {a₁ b₁ a₂ b₂ : has_abs.abs} (ha : a₁ a₂) (hb : b₁ b₂) :
a₁ b₁ a₂ b₂
theorem cau_seq.inf_equiv_inf {α : Type u_2} {a₁ b₁ a₂ b₂ : has_abs.abs} (ha : a₁ a₂) (hb : b₁ b₂) :
a₁ b₁ a₂ b₂
@[protected]
theorem cau_seq.sup_lt {α : Type u_2} {a b c : has_abs.abs} (ha : a < c) (hb : b < c) :
a b < c
@[protected]
theorem cau_seq.lt_inf {α : Type u_2} {a b c : has_abs.abs} (hb : a < b) (hc : a < c) :
a < b c
@[protected, simp]
theorem cau_seq.sup_idem {α : Type u_2} (a : has_abs.abs) :
a a = a
@[protected, simp]
theorem cau_seq.inf_idem {α : Type u_2} (a : has_abs.abs) :
a a = a
@[protected]
theorem cau_seq.sup_comm {α : Type u_2} (a b : has_abs.abs) :
a b = b a
@[protected]
theorem cau_seq.inf_comm {α : Type u_2} (a b : has_abs.abs) :
a b = b a
@[protected]
theorem cau_seq.sup_eq_right {α : Type u_2} {a b : has_abs.abs} (h : a b) :
a b b
@[protected]
theorem cau_seq.inf_eq_right {α : Type u_2} {a b : has_abs.abs} (h : b a) :
a b b
@[protected]
theorem cau_seq.sup_eq_left {α : Type u_2} {a b : has_abs.abs} (h : b a) :
a b a
@[protected]
theorem cau_seq.inf_eq_left {α : Type u_2} {a b : has_abs.abs} (h : a b) :
a b a
@[protected]
theorem cau_seq.le_sup_left {α : Type u_2} {a b : has_abs.abs} :
a a b
@[protected]
theorem cau_seq.inf_le_left {α : Type u_2} {a b : has_abs.abs} :
a b a
@[protected]
theorem cau_seq.le_sup_right {α : Type u_2} {a b : has_abs.abs} :
b a b
@[protected]
theorem cau_seq.inf_le_right {α : Type u_2} {a b : has_abs.abs} :
a b b
@[protected]
theorem cau_seq.sup_le {α : Type u_2} {a b c : has_abs.abs} (ha : a c) (hb : b c) :
a b c
@[protected]
theorem cau_seq.le_inf {α : Type u_2} {a b c : has_abs.abs} (hb : a b) (hc : a c) :
a b c

Note that `distrib_lattice (cau_seq α abs)` is not true because there is no `partial_order`.

@[protected]
theorem cau_seq.sup_inf_distrib_left {α : Type u_2} (a b c : has_abs.abs) :
a b c = (a b) (a c)
@[protected]
theorem cau_seq.sup_inf_distrib_right {α : Type u_2} (a b c : has_abs.abs) :
a b c = (a c) (b c)