def
cau_seq.completion.Cauchy
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Type u_2
Equations
def
cau_seq.completion.mk
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
cau_seq β abv → cau_seq.completion.Cauchy
Equations
@[simp]
theorem
cau_seq.completion.mk_eq_mk
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv) :
theorem
cau_seq.completion.mk_eq
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_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}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
@[instance]
def
cau_seq.completion.has_zero
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
@[instance]
def
cau_seq.completion.has_one
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
@[instance]
def
cau_seq.completion.inhabited
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
theorem
cau_seq.completion.of_rat_zero
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
theorem
cau_seq.completion.of_rat_one
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp]
theorem
cau_seq.completion.mk_eq_zero
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv} :
cau_seq.completion.mk f = 0 ↔ f.lim_zero
@[instance]
def
cau_seq.completion.has_add
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.has_add = {add := λ (x y : cau_seq.completion.Cauchy), quotient.lift_on₂ x y (λ (f g : cau_seq β abv), cau_seq.completion.mk (f + g)) cau_seq.completion.has_add._proof_1}
@[simp]
theorem
cau_seq.completion.mk_add
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
@[instance]
def
cau_seq.completion.has_neg
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.has_neg = {neg := λ (x : cau_seq.completion.Cauchy), quotient.lift_on x (λ (f : cau_seq β abv), cau_seq.completion.mk (-f)) cau_seq.completion.has_neg._proof_1}
@[simp]
theorem
cau_seq.completion.mk_neg
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv) :
@[instance]
def
cau_seq.completion.has_mul
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.has_mul = {mul := λ (x y : cau_seq.completion.Cauchy), quotient.lift_on₂ x y (λ (f g : cau_seq β abv), cau_seq.completion.mk (f * g)) cau_seq.completion.has_mul._proof_1}
@[simp]
theorem
cau_seq.completion.mk_mul
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
theorem
cau_seq.completion.of_rat_add
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
theorem
cau_seq.completion.of_rat_neg
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
theorem
cau_seq.completion.of_rat_mul
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
@[instance]
def
cau_seq.completion.comm_ring
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.comm_ring = {add := has_add.add cau_seq.completion.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg cau_seq.completion.has_neg, add_left_neg := _, add_comm := _, mul := has_mul.mul cau_seq.completion.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
theorem
cau_seq.completion.of_rat_sub
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
@[instance]
def
cau_seq.completion.has_inv
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.has_inv = {inv := λ (x : cau_seq.completion.Cauchy), 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.has_inv._proof_1}
@[simp]
theorem
cau_seq.completion.inv_zero
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
@[simp]
theorem
cau_seq.completion.inv_mk
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[field β]
{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}
[discrete_linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
theorem
cau_seq.completion.zero_ne_one
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
0 ≠ 1
theorem
cau_seq.completion.inv_mul_cancel
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
{x : cau_seq.completion.Cauchy} :
def
cau_seq.completion.field
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.field = {add := comm_ring.add cau_seq.completion.comm_ring, add_assoc := _, zero := comm_ring.zero cau_seq.completion.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg cau_seq.completion.comm_ring, add_left_neg := _, add_comm := _, mul := comm_ring.mul cau_seq.completion.comm_ring, mul_assoc := _, one := comm_ring.one cau_seq.completion.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := has_inv.inv cau_seq.completion.has_inv, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
theorem
cau_seq.completion.of_rat_inv
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
theorem
cau_seq.completion.of_rat_div
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
@[class]
structure
cau_seq.is_complete
{α : Type u_1}
[discrete_linear_ordered_field α]
(β : Type u_2)
[ring β]
(abv : β → α)
[is_absolute_value abv] :
Type
- is_complete : ∀ (s : cau_seq β abv), ∃ (b : β), s ≈ cau_seq.const abv b
theorem
cau_seq.complete
{α : Type u_1}
[discrete_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
def
cau_seq.lim
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv] :
cau_seq β abv → β
Equations
- s.lim = classical.some _
theorem
cau_seq.equiv_lim
{α : Type u_1}
[discrete_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}
[discrete_linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f : cau_seq β abv}
{x : β} :
cau_seq.const abv x ≈ f → x = f.lim
theorem
cau_seq.lim_eq_of_equiv_const
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f : cau_seq β abv}
{x : β} :
f ≈ cau_seq.const abv x → f.lim = x
theorem
cau_seq.lim_eq_lim_of_equiv
{α : Type u_1}
[discrete_linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f g : cau_seq β abv} :
@[simp]
theorem
cau_seq.lim_const
{α : Type u_1}
[discrete_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}
[discrete_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}
[discrete_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}
[discrete_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}
[discrete_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}
[discrete_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}
[discrete_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}
[discrete_linear_ordered_field α]
[cau_seq.is_complete α abs]
{f : cau_seq α abs}
{x : α} :
f ≤ cau_seq.const abs x → f.lim ≤ x
theorem
cau_seq.le_lim
{α : Type u_1}
[discrete_linear_ordered_field α]
[cau_seq.is_complete α abs]
{f : cau_seq α abs}
{x : α} :
cau_seq.const abs x ≤ f → x ≤ f.lim
theorem
cau_seq.lt_lim
{α : Type u_1}
[discrete_linear_ordered_field α]
[cau_seq.is_complete α abs]
{f : cau_seq α abs}
{x : α} :
cau_seq.const abs x < f → x < f.lim
theorem
cau_seq.lim_lt
{α : Type u_1}
[discrete_linear_ordered_field α]
[cau_seq.is_complete α abs]
{f : cau_seq α abs}
{x : α} :
f < cau_seq.const abs x → f.lim < x