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 saysf : ℕ → βis Cauchy.cau_seq: the type of Cauchy sequences valued in typeβwith respect to an absolute value functionabv.
Tags #
sequence, cauchy, abs val, absolute value
theorem
rat_mul_continuous_lemma
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
(abv : β → α)
[is_absolute_value abv]
{ε K₁ K₂ : α}
(ε0 : 0 < ε) :
theorem
is_cau_seq.add
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[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}
[linear_ordered_field α]
(β : 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
- cau_seq β abv = {f // is_cau_seq abv f}
Instances for cau_seq
- cau_seq.has_coe_to_fun
- cau_seq.has_add
- cau_seq.has_zero
- cau_seq.has_one
- cau_seq.inhabited
- cau_seq.has_mul
- cau_seq.has_neg
- cau_seq.has_sub
- cau_seq.has_smul
- cau_seq.is_scalar_tower
- cau_seq.add_group
- cau_seq.add_group_with_one
- cau_seq.nat.has_pow
- cau_seq.ring
- cau_seq.comm_ring
- cau_seq.equiv
- cau_seq.has_lt
- cau_seq.has_le
- cau_seq.preorder
- cau_seq.has_sup
- cau_seq.has_inf
@[protected, instance]
def
cau_seq.has_coe_to_fun
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α} :
has_coe_to_fun (cau_seq β abv) (λ (_x : cau_seq β abv), ℕ → β)
Equations
- cau_seq.has_coe_to_fun = {coe := subtype.val (λ (f : ℕ → β), is_cau_seq abv f)}
@[simp]
theorem
cau_seq.mk_to_fun
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
(f : ℕ → β)
(hf : is_cau_seq abv f) :
theorem
cau_seq.is_cau
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
(f : cau_seq β abv) :
is_cau_seq abv ⇑f
theorem
cau_seq.bounded
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv) :
@[protected, instance]
def
cau_seq.has_add
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp, norm_cast]
theorem
cau_seq.coe_add
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
def
cau_seq.const
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
(abv : β → α)
[is_absolute_value abv]
(x : β) :
cau_seq β abv
The constant Cauchy sequence.
Equations
- cau_seq.const abv x = ⟨λ (i : ℕ), x, _⟩
@[simp, norm_cast]
theorem
cau_seq.coe_const
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
⇑(cau_seq.const abv x) = function.const ℕ x
@[simp, norm_cast]
theorem
cau_seq.const_apply
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[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}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{x y : β} :
cau_seq.const abv x = cau_seq.const abv y ↔ x = y
@[protected, instance]
def
cau_seq.has_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.has_zero = {zero := cau_seq.const abv 0}
@[protected, instance]
def
cau_seq.has_one
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.has_one = {one := cau_seq.const abv 1}
@[protected, instance]
def
cau_seq.inhabited
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.inhabited = {default := 0}
@[simp, norm_cast]
theorem
cau_seq.coe_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp, norm_cast]
theorem
cau_seq.coe_one
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp, norm_cast]
theorem
cau_seq.zero_apply
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(i : ℕ) :
@[simp, norm_cast]
theorem
cau_seq.one_apply
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(i : ℕ) :
@[simp]
theorem
cau_seq.const_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
cau_seq.const abv 0 = 0
@[simp]
theorem
cau_seq.const_one
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
cau_seq.const abv 1 = 1
theorem
cau_seq.const_add
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
cau_seq.const abv (x + y) = cau_seq.const abv x + cau_seq.const abv y
@[protected, instance]
def
cau_seq.has_mul
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp, norm_cast]
theorem
cau_seq.coe_mul
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
theorem
cau_seq.const_mul
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
cau_seq.const abv (x * y) = cau_seq.const abv x * cau_seq.const abv y
@[protected, instance]
def
cau_seq.has_neg
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp, norm_cast]
theorem
cau_seq.coe_neg
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv) :
@[simp, norm_cast]
theorem
cau_seq.neg_apply
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv)
(i : ℕ) :
theorem
cau_seq.const_neg
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
cau_seq.const abv (-x) = -cau_seq.const abv x
@[simp, norm_cast]
theorem
cau_seq.coe_sub
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
theorem
cau_seq.const_sub
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
cau_seq.const abv (x - y) = cau_seq.const abv x - cau_seq.const abv y
@[protected, instance]
def
cau_seq.has_smul
{G : Type u_1}
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
[has_smul G β]
[is_scalar_tower G β β] :
@[simp, norm_cast]
theorem
cau_seq.coe_smul
{G : Type u_1}
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
[has_smul G β]
[is_scalar_tower G β β]
(a : G)
(f : cau_seq β abv) :
@[simp, norm_cast]
theorem
cau_seq.smul_apply
{G : Type u_1}
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
[has_smul G β]
[is_scalar_tower G β β]
(a : G)
(f : cau_seq β abv)
(i : ℕ) :
theorem
cau_seq.const_smul
{G : Type u_1}
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
[has_smul G β]
[is_scalar_tower G β β]
(a : G)
(x : β) :
cau_seq.const abv (a • x) = a • cau_seq.const abv x
@[protected, instance]
def
cau_seq.is_scalar_tower
{G : Type u_1}
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
[has_smul G β]
[is_scalar_tower G β β] :
is_scalar_tower G (cau_seq β abv) (cau_seq β abv)
@[protected, instance]
def
cau_seq.add_group
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.add_group = function.injective.add_group coe cau_seq.add_group._proof_3 cau_seq.add_group._proof_4 cau_seq.coe_add cau_seq.coe_neg cau_seq.coe_sub cau_seq.add_group._proof_5 cau_seq.add_group._proof_6
@[protected, instance]
def
cau_seq.add_group_with_one
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
add_group_with_one (cau_seq β abv)
Equations
- cau_seq.add_group_with_one = {int_cast := λ (n : ℤ), cau_seq.const abv ↑n, add := add_group.add cau_seq.add_group, add_assoc := _, zero := add_group.zero cau_seq.add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul cau_seq.add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg cau_seq.add_group, sub := add_group.sub cau_seq.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul cau_seq.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := λ (n : ℕ), cau_seq.const abv ↑n, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
@[protected, instance]
def
cau_seq.nat.has_pow
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp, norm_cast]
theorem
cau_seq.coe_pow
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv)
(n : ℕ) :
@[simp, norm_cast]
theorem
cau_seq.pow_apply
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv)
(n i : ℕ) :
theorem
cau_seq.const_pow
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β)
(n : ℕ) :
cau_seq.const abv (x ^ n) = cau_seq.const abv x ^ n
@[protected, instance]
def
cau_seq.ring
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.ring = function.injective.ring coe cau_seq.ring._proof_3 cau_seq.ring._proof_4 cau_seq.ring._proof_5 cau_seq.coe_add cau_seq.coe_mul cau_seq.coe_neg cau_seq.coe_sub cau_seq.ring._proof_6 cau_seq.ring._proof_7 cau_seq.coe_pow cau_seq.ring._proof_8 cau_seq.ring._proof_9
@[protected, instance]
def
cau_seq.comm_ring
{α : Type u_2}
[linear_ordered_field α]
{β : Type u_1}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.comm_ring = {add := ring.add cau_seq.ring, add_assoc := _, zero := ring.zero cau_seq.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul cau_seq.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg cau_seq.ring, sub := ring.sub cau_seq.ring, sub_eq_add_neg := _, zsmul := ring.zsmul cau_seq.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast cau_seq.ring, nat_cast := ring.nat_cast cau_seq.ring, one := ring.one cau_seq.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul cau_seq.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow cau_seq.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
theorem
cau_seq.add_lim_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(hf : f.lim_zero)
(hg : g.lim_zero) :
theorem
cau_seq.mul_lim_zero_right
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv)
{g : cau_seq β abv}
(hg : g.lim_zero) :
theorem
cau_seq.mul_lim_zero_left
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(g : cau_seq β abv)
(hg : f.lim_zero) :
theorem
cau_seq.neg_lim_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : f.lim_zero) :
theorem
cau_seq.sub_lim_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(hf : f.lim_zero)
(hg : g.lim_zero) :
theorem
cau_seq.lim_zero_sub_rev
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(hfg : (f - g).lim_zero) :
theorem
cau_seq.zero_lim_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
0.lim_zero
theorem
cau_seq.const_lim_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{x : β} :
(cau_seq.const abv x).lim_zero ↔ x = 0
@[protected, instance]
def
cau_seq.equiv
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv] :
theorem
cau_seq.add_equiv_add
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f1 f2 g1 g2 : cau_seq β abv}
(hf : f1 ≈ f2)
(hg : g1 ≈ g2) :
theorem
cau_seq.neg_equiv_neg
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(hf : f ≈ g) :
theorem
cau_seq.sub_equiv_sub
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f1 f2 g1 g2 : cau_seq β abv}
(hf : f1 ≈ f2)
(hg : g1 ≈ g2) :
theorem
cau_seq.lim_zero_congr
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(h : f ≈ g) :
theorem
cau_seq.not_lim_zero_of_not_congr_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : ¬f ≈ 0) :
theorem
cau_seq.mul_equiv_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(g : cau_seq β abv)
{f : cau_seq β abv}
(hf : f ≈ 0) :
theorem
cau_seq.mul_equiv_zero'
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
(g : cau_seq β abv)
{f : cau_seq β abv}
(hf : f ≈ 0) :
theorem
cau_seq.const_equiv
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{x y : β} :
cau_seq.const abv x ≈ cau_seq.const abv y ↔ x = y
theorem
cau_seq.mul_equiv_mul
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f1 f2 g1 g2 : cau_seq β abv}
(hf : f1 ≈ f2)
(hg : g1 ≈ g2) :
theorem
cau_seq.smul_equiv_smul
{G : Type u_1}
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
[has_smul G β]
[is_scalar_tower G β β]
{f1 f2 : cau_seq β abv}
(c : G)
(hf : f1 ≈ f2) :
theorem
cau_seq.pow_equiv_pow
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f1 f2 : cau_seq β abv}
(hf : f1 ≈ f2)
(n : ℕ) :
theorem
cau_seq.one_not_equiv_zero
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[ring β]
[is_domain β]
(abv : β → α)
[is_absolute_value abv] :
¬cau_seq.const abv 1 ≈ cau_seq.const abv 0
def
cau_seq.inv
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv)
(hf : ¬f.lim_zero) :
cau_seq β abv
Given a Cauchy sequence f with nonzero limit, create a Cauchy sequence with values equal to
the inverses of the values of f.
@[simp, norm_cast]
theorem
cau_seq.coe_inv
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : ¬f.lim_zero) :
@[simp, norm_cast]
theorem
cau_seq.inv_apply
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : ¬f.lim_zero)
(i : ℕ) :
theorem
cau_seq.inv_mul_cancel
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : ¬f.lim_zero) :
theorem
cau_seq.mul_inv_cancel
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : ¬f.lim_zero) :
theorem
cau_seq.const_inv
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
{x : β}
(hx : x ≠ 0) :
cau_seq.const abv x⁻¹ = (cau_seq.const abv x).inv _
theorem
cau_seq.not_lim_zero_of_pos
{α : Type u_2}
[linear_ordered_field α]
{f : cau_seq α has_abs.abs} :
theorem
cau_seq.const_pos
{α : Type u_2}
[linear_ordered_field α]
{x : α} :
(cau_seq.const has_abs.abs x).pos ↔ 0 < x
theorem
cau_seq.pos_add_lim_zero
{α : Type u_2}
[linear_ordered_field α]
{f g : cau_seq α has_abs.abs} :
@[protected]
@[protected, instance]
Equations
- cau_seq.has_lt = {lt := λ (f g : cau_seq α has_abs.abs), (g - f).pos}
@[protected, instance]
Equations
- cau_seq.has_le = {le := λ (f g : cau_seq α has_abs.abs), f < g ∨ f ≈ g}
theorem
cau_seq.lt_of_lt_of_eq
{α : Type u_2}
[linear_ordered_field α]
{f g h : cau_seq α has_abs.abs}
(fg : f < g)
(gh : g ≈ h) :
f < h
theorem
cau_seq.lt_of_eq_of_lt
{α : Type u_2}
[linear_ordered_field α]
{f g h : cau_seq α has_abs.abs}
(fg : f ≈ g)
(gh : g < h) :
f < h
theorem
cau_seq.lt_trans
{α : Type u_2}
[linear_ordered_field α]
{f g h : cau_seq α has_abs.abs}
(fg : f < g)
(gh : g < h) :
f < h
theorem
cau_seq.le_of_eq_of_le
{α : Type u_2}
[linear_ordered_field α]
{f g h : cau_seq α has_abs.abs}
(hfg : f ≈ g)
(hgh : g ≤ h) :
f ≤ h
theorem
cau_seq.le_of_le_of_eq
{α : Type u_2}
[linear_ordered_field α]
{f g h : cau_seq α has_abs.abs}
(hfg : f ≤ g)
(hgh : g ≈ h) :
f ≤ h
@[protected, instance]
Equations
- cau_seq.preorder = {le := λ (f g : cau_seq α has_abs.abs), f < g ∨ f ≈ g, lt := has_lt.lt cau_seq.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
theorem
cau_seq.le_antisymm
{α : Type u_2}
[linear_ordered_field α]
{f g : cau_seq α has_abs.abs}
(fg : f ≤ g)
(gf : g ≤ f) :
f ≈ g
theorem
cau_seq.const_lt
{α : Type u_2}
[linear_ordered_field α]
{x y : α} :
cau_seq.const has_abs.abs x < cau_seq.const has_abs.abs y ↔ x < y
theorem
cau_seq.const_le
{α : Type u_2}
[linear_ordered_field α]
{x y : α} :
cau_seq.const has_abs.abs x ≤ cau_seq.const has_abs.abs y ↔ x ≤ y
theorem
cau_seq.exists_gt
{α : Type u_2}
[linear_ordered_field α]
(f : cau_seq α has_abs.abs) :
∃ (a : α), f < cau_seq.const has_abs.abs a
theorem
cau_seq.exists_lt
{α : Type u_2}
[linear_ordered_field α]
(f : cau_seq α has_abs.abs) :
∃ (a : α), cau_seq.const has_abs.abs a < f
@[protected, instance]
Equations
- cau_seq.has_sup = {sup := λ (f g : cau_seq α has_abs.abs), ⟨⇑f ⊔ ⇑g, _⟩}
@[protected, instance]
Equations
- cau_seq.has_inf = {inf := λ (f g : cau_seq α has_abs.abs), ⟨⇑f ⊓ ⇑g, _⟩}
@[simp, norm_cast]
@[simp, norm_cast]
theorem
cau_seq.sup_lim_zero
{α : Type u_2}
[linear_ordered_field α]
{f g : cau_seq α has_abs.abs}
(hf : f.lim_zero)
(hg : g.lim_zero) :
theorem
cau_seq.inf_lim_zero
{α : Type u_2}
[linear_ordered_field α]
{f g : cau_seq α has_abs.abs}
(hf : f.lim_zero)
(hg : g.lim_zero) :
theorem
cau_seq.sup_equiv_sup
{α : Type u_2}
[linear_ordered_field α]
{a₁ b₁ a₂ b₂ : cau_seq α has_abs.abs}
(ha : a₁ ≈ a₂)
(hb : b₁ ≈ b₂) :
theorem
cau_seq.inf_equiv_inf
{α : Type u_2}
[linear_ordered_field α]
{a₁ b₁ a₂ b₂ : cau_seq α has_abs.abs}
(ha : a₁ ≈ a₂)
(hb : b₁ ≈ b₂) :
@[protected]
theorem
cau_seq.sup_lt
{α : Type u_2}
[linear_ordered_field α]
{a b c : cau_seq α has_abs.abs}
(ha : a < c)
(hb : b < c) :
@[protected]
theorem
cau_seq.lt_inf
{α : Type u_2}
[linear_ordered_field α]
{a b c : cau_seq α has_abs.abs}
(hb : a < b)
(hc : a < c) :
@[protected, simp]
@[protected, simp]
@[protected]
@[protected]
@[protected]
theorem
cau_seq.sup_eq_right
{α : Type u_2}
[linear_ordered_field α]
{a b : cau_seq α has_abs.abs}
(h : a ≤ b) :
@[protected]
theorem
cau_seq.inf_eq_right
{α : Type u_2}
[linear_ordered_field α]
{a b : cau_seq α has_abs.abs}
(h : b ≤ a) :
@[protected]
theorem
cau_seq.sup_eq_left
{α : Type u_2}
[linear_ordered_field α]
{a b : cau_seq α has_abs.abs}
(h : b ≤ a) :
@[protected]
theorem
cau_seq.inf_eq_left
{α : Type u_2}
[linear_ordered_field α]
{a b : cau_seq α has_abs.abs}
(h : a ≤ b) :
@[protected]
@[protected]
@[protected]
theorem
cau_seq.le_sup_right
{α : Type u_2}
[linear_ordered_field α]
{a b : cau_seq α has_abs.abs} :
@[protected]
theorem
cau_seq.inf_le_right
{α : Type u_2}
[linear_ordered_field α]
{a b : cau_seq α has_abs.abs} :
@[protected]
theorem
cau_seq.sup_le
{α : Type u_2}
[linear_ordered_field α]
{a b c : cau_seq α has_abs.abs}
(ha : a ≤ c)
(hb : b ≤ c) :
@[protected]
theorem
cau_seq.le_inf
{α : Type u_2}
[linear_ordered_field α]
{a b c : cau_seq α has_abs.abs}
(hb : a ≤ b)
(hc : a ≤ 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}
[linear_ordered_field α]
(a b c : cau_seq α has_abs.abs) :
@[protected]
theorem
cau_seq.sup_inf_distrib_right
{α : Type u_2}
[linear_ordered_field α]
(a b c : cau_seq α has_abs.abs) :