mathlib documentation

data.real.cau_seq_completion

def cau_seq.completion.Cauchy {α : Type u_1} [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} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :

Equations
@[simp]
theorem cau_seq.completion.mk_eq_mk {α : Type u_1} [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} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] {f g : cau_seq β abv} :

def cau_seq.completion.of_rat {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :

Equations
@[instance]
def cau_seq.completion.has_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :

Equations
@[instance]
def cau_seq.completion.inhabited {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :

Equations
theorem cau_seq.completion.of_rat_zero {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :

theorem cau_seq.completion.of_rat_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :

@[simp]
theorem cau_seq.completion.mk_eq_zero {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] {f : cau_seq β abv} :

@[instance]
def cau_seq.completion.has_add {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :

Equations
@[simp]
theorem cau_seq.completion.mk_add {α : Type u_1} [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} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :

Equations
@[simp]
theorem cau_seq.completion.mk_neg {α : Type u_1} [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} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :

Equations
@[simp]
theorem cau_seq.completion.mk_mul {α : Type u_1} [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} [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} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (x : β) :

theorem cau_seq.completion.of_rat_mul {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (x y : β) :

theorem cau_seq.completion.of_rat_sub {α : Type u_1} [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} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :

Equations
@[simp]
theorem cau_seq.completion.inv_zero {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
0⁻¹ = 0

@[simp]
theorem cau_seq.completion.inv_mk {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] {f : cau_seq β abv} (hf : ¬f.lim_zero) :

theorem cau_seq.completion.cau_seq_zero_ne_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
¬0 1

theorem cau_seq.completion.zero_ne_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
0 1

theorem cau_seq.completion.inv_mul_cancel {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] {x : cau_seq.completion.Cauchy} :
x 0x⁻¹ * x = 1

theorem cau_seq.completion.of_rat_inv {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] (x : β) :

theorem cau_seq.completion.of_rat_div {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] (x y : β) :

@[class]
structure cau_seq.is_complete {α : Type u_1} [linear_ordered_field α] (β : Type u_2) [ring β] (abv : β → α) [is_absolute_value abv] :
Type

Instances
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

def cau_seq.lim {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] :
cau_seq β abv → β

Equations
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) :

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 : β} :
cau_seq.const abv x fx = f.lim

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 : β} :
f cau_seq.const abv xf.lim = 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} :
f gf.lim = g.lim

@[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) :
f.lim + g.lim = (f + g).lim

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) :
(f.lim) * g.lim = (f * g).lim

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 : β) :
(f.lim) * x = (f * cau_seq.const abv x).lim

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) :
(-f).lim = -f.lim

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) :
(f.inv hf).lim = (f.lim)⁻¹

theorem cau_seq.lim_le {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α abs] {f : cau_seq α abs} {x : α} :

theorem cau_seq.le_lim {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α abs] {f : cau_seq α abs} {x : α} :

theorem cau_seq.lt_lim {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α abs] {f : cau_seq α abs} {x : α} :
cau_seq.const abs x < fx < f.lim

theorem cau_seq.lim_lt {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α abs] {f : cau_seq α abs} {x : α} :
f < cau_seq.const abs xf.lim < x