Cauchy completion #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file generalizes the Cauchy completion of (ℚ, abs) to the completion of a ring
with absolute value.
def
cau_seq.completion.Cauchy
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
(abv : β → α)
[is_absolute_value abv] :
Type u_2
The Cauchy completion of a ring with absolute value.
Equations
Instances for cau_seq.completion.Cauchy
- cau_seq.completion.Cauchy.has_zero
- cau_seq.completion.Cauchy.has_one
- cau_seq.completion.Cauchy.inhabited
- cau_seq.completion.Cauchy.has_add
- cau_seq.completion.Cauchy.has_neg
- cau_seq.completion.Cauchy.has_mul
- cau_seq.completion.Cauchy.has_sub
- cau_seq.completion.Cauchy.has_smul
- cau_seq.completion.nat.has_pow
- cau_seq.completion.Cauchy.has_nat_cast
- cau_seq.completion.Cauchy.has_int_cast
- cau_seq.completion.Cauchy.ring
- cau_seq.completion.Cauchy.comm_ring
- cau_seq.completion.Cauchy.has_rat_cast
- cau_seq.completion.Cauchy.has_inv
- cau_seq.completion.Cauchy.division_ring
- cau_seq.completion.Cauchy.has_repr
- cau_seq.completion.Cauchy.field
def
cau_seq.completion.mk
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
cau_seq β abv → cau_seq.completion.Cauchy abv
The map from Cauchy sequences into the Cauchy completion.
Equations
@[simp]
theorem
cau_seq.completion.mk_eq_mk
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv) :
theorem
cau_seq.completion.mk_eq
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv} :
cau_seq.completion.mk f = cau_seq.completion.mk g ↔ f ≈ g
def
cau_seq.completion.of_rat
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
The map from the original ring into the Cauchy completion.
Equations
@[protected, instance]
def
cau_seq.completion.Cauchy.has_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
@[protected, instance]
def
cau_seq.completion.Cauchy.has_one
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
@[protected, instance]
def
cau_seq.completion.Cauchy.inhabited
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
theorem
cau_seq.completion.of_rat_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
theorem
cau_seq.completion.of_rat_one
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp]
theorem
cau_seq.completion.mk_eq_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv} :
cau_seq.completion.mk f = 0 ↔ f.lim_zero
@[protected, instance]
def
cau_seq.completion.Cauchy.has_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_add = {add := quotient.map₂ has_add.add cau_seq.completion.Cauchy.has_add._proof_1}
@[simp]
theorem
cau_seq.completion.mk_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
@[protected, instance]
def
cau_seq.completion.Cauchy.has_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_neg = {neg := quotient.map has_neg.neg cau_seq.completion.Cauchy.has_neg._proof_1}
@[simp]
theorem
cau_seq.completion.mk_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv) :
@[protected, instance]
def
cau_seq.completion.Cauchy.has_mul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_mul = {mul := quotient.map₂ has_mul.mul cau_seq.completion.Cauchy.has_mul._proof_1}
@[simp]
theorem
cau_seq.completion.mk_mul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
@[protected, instance]
def
cau_seq.completion.Cauchy.has_sub
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_sub = {sub := quotient.map₂ has_sub.sub cau_seq.completion.Cauchy.has_sub._proof_1}
@[simp]
theorem
cau_seq.completion.mk_sub
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
@[protected, instance]
def
cau_seq.completion.Cauchy.has_smul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{γ : Type u_3}
[has_smul γ β]
[is_scalar_tower γ β β] :
has_smul γ (cau_seq.completion.Cauchy abv)
Equations
- cau_seq.completion.Cauchy.has_smul = {smul := λ (c : γ), quotient.map (has_smul.smul c) _}
@[simp]
theorem
cau_seq.completion.mk_smul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{γ : Type u_3}
[has_smul γ β]
[is_scalar_tower γ β β]
(c : γ)
(f : cau_seq β abv) :
c • cau_seq.completion.mk f = cau_seq.completion.mk (c • f)
@[protected, instance]
def
cau_seq.completion.nat.has_pow
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.nat.has_pow = {pow := λ (x : cau_seq.completion.Cauchy abv) (n : ℕ), quotient.map (λ (_x : cau_seq β abv), _x ^ n) _ x}
@[simp]
theorem
cau_seq.completion.mk_pow
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(n : ℕ)
(f : cau_seq β abv) :
cau_seq.completion.mk f ^ n = cau_seq.completion.mk (f ^ n)
@[protected, instance]
def
cau_seq.completion.Cauchy.has_nat_cast
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_nat_cast = {nat_cast := λ (n : ℕ), cau_seq.completion.mk ↑n}
@[protected, instance]
def
cau_seq.completion.Cauchy.has_int_cast
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_int_cast = {int_cast := λ (n : ℤ), cau_seq.completion.mk ↑n}
@[simp]
theorem
cau_seq.completion.of_rat_nat_cast
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(n : ℕ) :
@[simp]
theorem
cau_seq.completion.of_rat_int_cast
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(z : ℤ) :
theorem
cau_seq.completion.of_rat_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
theorem
cau_seq.completion.of_rat_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
theorem
cau_seq.completion.of_rat_mul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
@[protected, instance]
def
cau_seq.completion.Cauchy.ring
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.ring = function.surjective.ring cau_seq.completion.mk cau_seq.completion.Cauchy.ring._proof_3 cau_seq.completion.Cauchy.ring._proof_4 cau_seq.completion.Cauchy.ring._proof_5 cau_seq.completion.Cauchy.ring._proof_6 cau_seq.completion.Cauchy.ring._proof_7 cau_seq.completion.Cauchy.ring._proof_8 cau_seq.completion.Cauchy.ring._proof_9 cau_seq.completion.Cauchy.ring._proof_10 cau_seq.completion.Cauchy.ring._proof_11 cau_seq.completion.Cauchy.ring._proof_12 cau_seq.completion.Cauchy.ring._proof_13 cau_seq.completion.Cauchy.ring._proof_14
def
cau_seq.completion.of_rat_ring_hom
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
β →+* cau_seq.completion.Cauchy abv
cau_seq.completion.of_rat as a ring_hom
Equations
- cau_seq.completion.of_rat_ring_hom = {to_fun := cau_seq.completion.of_rat _inst_3, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
cau_seq.completion.of_rat_ring_hom_apply
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
theorem
cau_seq.completion.of_rat_sub
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
@[protected, instance]
def
cau_seq.completion.Cauchy.comm_ring
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.comm_ring = function.surjective.comm_ring cau_seq.completion.mk cau_seq.completion.Cauchy.comm_ring._proof_3 cau_seq.completion.Cauchy.comm_ring._proof_4 cau_seq.completion.Cauchy.comm_ring._proof_5 cau_seq.completion.Cauchy.comm_ring._proof_6 cau_seq.completion.Cauchy.comm_ring._proof_7 cau_seq.completion.Cauchy.comm_ring._proof_8 cau_seq.completion.Cauchy.comm_ring._proof_9 cau_seq.completion.Cauchy.comm_ring._proof_10 cau_seq.completion.Cauchy.comm_ring._proof_11 cau_seq.completion.Cauchy.comm_ring._proof_12 cau_seq.completion.Cauchy.comm_ring._proof_13 cau_seq.completion.Cauchy.comm_ring._proof_14
@[protected, instance]
def
cau_seq.completion.Cauchy.has_rat_cast
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_rat_cast = {rat_cast := λ (q : ℚ), cau_seq.completion.of_rat ↑q}
@[simp]
theorem
cau_seq.completion.of_rat_rat_cast
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
(q : ℚ) :
@[protected, instance]
noncomputable
def
cau_seq.completion.Cauchy.has_inv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_inv = {inv := λ (x : cau_seq.completion.Cauchy abv), quotient.lift_on x (λ (f : cau_seq β abv), cau_seq.completion.mk (dite f.lim_zero (λ (h : f.lim_zero), 0) (λ (h : ¬f.lim_zero), f.inv h))) cau_seq.completion.Cauchy.has_inv._proof_1}
@[simp]
theorem
cau_seq.completion.inv_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp]
theorem
cau_seq.completion.inv_mk
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : ¬f.lim_zero) :
(cau_seq.completion.mk f)⁻¹ = cau_seq.completion.mk (f.inv hf)
theorem
cau_seq.completion.cau_seq_zero_ne_one
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv] :
theorem
cau_seq.completion.zero_ne_one
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv] :
0 ≠ 1
@[protected]
theorem
cau_seq.completion.inv_mul_cancel
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
{x : cau_seq.completion.Cauchy abv} :
@[protected]
theorem
cau_seq.completion.mul_inv_cancel
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
{x : cau_seq.completion.Cauchy abv} :
theorem
cau_seq.completion.of_rat_inv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
@[protected, instance]
noncomputable
def
cau_seq.completion.Cauchy.division_ring
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv] :
The Cauchy completion forms a division ring.
Equations
- cau_seq.completion.Cauchy.division_ring = {add := ring.add cau_seq.completion.Cauchy.ring, add_assoc := _, zero := ring.zero cau_seq.completion.Cauchy.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul cau_seq.completion.Cauchy.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg cau_seq.completion.Cauchy.ring, sub := ring.sub cau_seq.completion.Cauchy.ring, sub_eq_add_neg := _, zsmul := ring.zsmul cau_seq.completion.Cauchy.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast cau_seq.completion.Cauchy.ring, nat_cast := ring.nat_cast cau_seq.completion.Cauchy.ring, one := ring.one cau_seq.completion.Cauchy.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul cau_seq.completion.Cauchy.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow cau_seq.completion.Cauchy.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := has_inv.inv cau_seq.completion.Cauchy.has_inv, div := div_inv_monoid.div._default ring.mul cau_seq.completion.Cauchy.division_ring._proof_23 ring.one cau_seq.completion.Cauchy.division_ring._proof_24 cau_seq.completion.Cauchy.division_ring._proof_25 ring.npow cau_seq.completion.Cauchy.division_ring._proof_26 cau_seq.completion.Cauchy.division_ring._proof_27 has_inv.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default ring.mul cau_seq.completion.Cauchy.division_ring._proof_29 ring.one cau_seq.completion.Cauchy.division_ring._proof_30 cau_seq.completion.Cauchy.division_ring._proof_31 ring.npow cau_seq.completion.Cauchy.division_ring._proof_32 cau_seq.completion.Cauchy.division_ring._proof_33 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := λ (q : ℚ), cau_seq.completion.of_rat ↑q, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec (λ (q : ℚ), cau_seq.completion.of_rat ↑q) (distrib.to_has_mul (cau_seq.completion.Cauchy abv)), qsmul_eq_mul' := _}
theorem
cau_seq.completion.of_rat_div
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[division_ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
@[protected, instance]
noncomputable
def
cau_seq.completion.Cauchy.field
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
The Cauchy completion forms a field.
Equations
- cau_seq.completion.Cauchy.field = {add := division_ring.add cau_seq.completion.Cauchy.division_ring, add_assoc := _, zero := division_ring.zero cau_seq.completion.Cauchy.division_ring, zero_add := _, add_zero := _, nsmul := division_ring.nsmul cau_seq.completion.Cauchy.division_ring, nsmul_zero' := _, nsmul_succ' := _, neg := division_ring.neg cau_seq.completion.Cauchy.division_ring, sub := division_ring.sub cau_seq.completion.Cauchy.division_ring, sub_eq_add_neg := _, zsmul := division_ring.zsmul cau_seq.completion.Cauchy.division_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := division_ring.int_cast cau_seq.completion.Cauchy.division_ring, nat_cast := division_ring.nat_cast cau_seq.completion.Cauchy.division_ring, one := division_ring.one cau_seq.completion.Cauchy.division_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := division_ring.mul cau_seq.completion.Cauchy.division_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := division_ring.npow cau_seq.completion.Cauchy.division_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv cau_seq.completion.Cauchy.division_ring, div := division_ring.div cau_seq.completion.Cauchy.division_ring, div_eq_mul_inv := _, zpow := division_ring.zpow cau_seq.completion.Cauchy.division_ring, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := division_ring.rat_cast cau_seq.completion.Cauchy.division_ring, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul cau_seq.completion.Cauchy.division_ring, qsmul_eq_mul' := _}
@[class]
structure
cau_seq.is_complete
{α : Type u_1}
[linear_ordered_field α]
(β : Type u_2)
[ring β]
(abv : β → α)
[is_absolute_value abv] :
Prop
A class stating that a ring with an absolute value is complete, i.e. every Cauchy sequence has a limit.
Instances of this typeclass
theorem
cau_seq.complete
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(s : cau_seq β abv) :
∃ (b : β), s ≈ cau_seq.const abv b
noncomputable
def
cau_seq.lim
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(s : cau_seq β abv) :
β
The limit of a Cauchy sequence in a complete ring. Chosen non-computably.
Equations
- s.lim = classical.some _
theorem
cau_seq.equiv_lim
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(s : cau_seq β abv) :
s ≈ cau_seq.const abv s.lim
theorem
cau_seq.eq_lim_of_const_equiv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f : cau_seq β abv}
{x : β}
(h : cau_seq.const abv x ≈ f) :
theorem
cau_seq.lim_eq_of_equiv_const
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f : cau_seq β abv}
{x : β}
(h : f ≈ cau_seq.const abv x) :
theorem
cau_seq.lim_eq_lim_of_equiv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f g : cau_seq β abv}
(h : f ≈ g) :
@[simp]
theorem
cau_seq.lim_const
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(x : β) :
(cau_seq.const abv x).lim = x
theorem
cau_seq.lim_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(f g : cau_seq β abv) :
theorem
cau_seq.lim_mul_lim
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(f g : cau_seq β abv) :
theorem
cau_seq.lim_mul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(f : cau_seq β abv)
(x : β) :
theorem
cau_seq.lim_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(f : cau_seq β abv) :
theorem
cau_seq.lim_eq_zero_iff
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(f : cau_seq β abv) :
theorem
cau_seq.lim_inv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f : cau_seq β abv}
(hf : ¬f.lim_zero) :
theorem
cau_seq.lim_le
{α : Type u_1}
[linear_ordered_field α]
[cau_seq.is_complete α has_abs.abs]
{f : cau_seq α has_abs.abs}
{x : α}
(h : f ≤ cau_seq.const has_abs.abs x) :
theorem
cau_seq.le_lim
{α : Type u_1}
[linear_ordered_field α]
[cau_seq.is_complete α has_abs.abs]
{f : cau_seq α has_abs.abs}
{x : α}
(h : cau_seq.const has_abs.abs x ≤ f) :
theorem
cau_seq.lt_lim
{α : Type u_1}
[linear_ordered_field α]
[cau_seq.is_complete α has_abs.abs]
{f : cau_seq α has_abs.abs}
{x : α}
(h : cau_seq.const has_abs.abs x < f) :
theorem
cau_seq.lim_lt
{α : Type u_1}
[linear_ordered_field α]
[cau_seq.is_complete α has_abs.abs]
{f : cau_seq α has_abs.abs}
{x : α}
(h : f < cau_seq.const has_abs.abs x) :