Cauchy completion #

This file generalizes the Cauchy completion of (ℚ, abs) to the completion of a ring with absolute value.

def CauSeq.Completion.Cauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] (abv : β → α) [inst : IsAbsoluteValue abv] :

Type u_2

The Cauchy completion of a ring with absolute value.

Equations

CauSeq.Completion.Cauchy abv = Quotient CauSeq.equiv

source

ink

def CauSeq.Completion.mk {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

CauSeq β abv → CauSeq.Completion.Cauchy abv

The map from Cauchy sequences into the Cauchy completion.

Equations

CauSeq.Completion.mk = Quotient.mk''

source

ink

@[simp]

theorem CauSeq.Completion.mk_eq_mk {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) :

Quotient.mk CauSeq.equiv f = CauSeq.Completion.mk f

source

ink

theorem CauSeq.Completion.mk_eq {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} :

CauSeq.Completion.mk f = CauSeq.Completion.mk g ↔ f ≈ g

source

ink

def CauSeq.Completion.ofRat {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) :

CauSeq.Completion.Cauchy abv

The map from the original ring into the Cauchy completion.

Equations

CauSeq.Completion.ofRat x = CauSeq.Completion.mk (CauSeq.const abv x)

source

ink

instance CauSeq.Completion.instZeroCauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

Zero (CauSeq.Completion.Cauchy abv)

Equations

CauSeq.Completion.instZeroCauchy = { zero := CauSeq.Completion.ofRat 0 }

source

ink

instance CauSeq.Completion.instOneCauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

One (CauSeq.Completion.Cauchy abv)

Equations

CauSeq.Completion.instOneCauchy = { one := CauSeq.Completion.ofRat 1 }

source

ink

instance CauSeq.Completion.instInhabitedCauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

Inhabited (CauSeq.Completion.Cauchy abv)

Equations

CauSeq.Completion.instInhabitedCauchy = { default := 0 }

source

ink

theorem CauSeq.Completion.ofRat_zero {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

CauSeq.Completion.ofRat 0 = 0

source

ink

theorem CauSeq.Completion.ofRat_one {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

CauSeq.Completion.ofRat 1 = 1

source

ink

@[simp]

theorem CauSeq.Completion.mk_eq_zero {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} :

CauSeq.Completion.mk f = 0 ↔ CauSeq.LimZero f

source

ink

instance CauSeq.Completion.instAddCauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

Add (CauSeq.Completion.Cauchy abv)

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem CauSeq.Completion.mk_add {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) :

CauSeq.Completion.mk f + CauSeq.Completion.mk g = CauSeq.Completion.mk (f + g)

source

ink

instance CauSeq.Completion.instNegCauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

Neg (CauSeq.Completion.Cauchy abv)

Equations

CauSeq.Completion.instNegCauchy = { neg := Quotient.map Neg.neg (_ : ∀ (x x_1 : CauSeq β abv), x ≈ x_1 → -x ≈ -x_1) }

source

ink

@[simp]

theorem CauSeq.Completion.mk_neg {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) :

-CauSeq.Completion.mk f = CauSeq.Completion.mk (-f)

source

ink

instance CauSeq.Completion.instMulCauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

Mul (CauSeq.Completion.Cauchy abv)

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem CauSeq.Completion.mk_mul {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) :

CauSeq.Completion.mk f * CauSeq.Completion.mk g = CauSeq.Completion.mk (f * g)

source

ink

instance CauSeq.Completion.instSubCauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

Sub (CauSeq.Completion.Cauchy abv)

Equations

CauSeq.Completion.instSubCauchy = { sub := Quotient.map₂ Sub.sub (_ : ∀ (x x_1 : CauSeq β abv), x ≈ x_1 → ∀ (x_2 x_3 : CauSeq β abv), x_2 ≈ x_3 → x - x_2 ≈ x_1 - x_3) }

source

ink

@[simp]

theorem CauSeq.Completion.mk_sub {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) :

CauSeq.Completion.mk f - CauSeq.Completion.mk g = CauSeq.Completion.mk (f - g)

source

ink

instance CauSeq.Completion.instSMulCauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {γ : Type u_3} [inst : SMul γ β] [inst : IsScalarTower γ β β] :

SMul γ (CauSeq.Completion.Cauchy abv)

Equations

CauSeq.Completion.instSMulCauchy = { smul := fun c => Quotient.map ((fun x x_1 => x • x_1) c) (_ : ∀ (x x_1 : CauSeq β abv), x ≈ x_1 → c • x ≈ c • x_1) }

source

ink

@[simp]

theorem CauSeq.Completion.mk_smul {α : Type u_3} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] {γ : Type u_1} [inst : SMul γ β] [inst : IsScalarTower γ β β] (c : γ) (f : CauSeq β abv) :

c • CauSeq.Completion.mk f = CauSeq.Completion.mk (c • f)

source

ink

instance CauSeq.Completion.instPowCauchyNat {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

Pow (CauSeq.Completion.Cauchy abv) ℕ

Equations

CauSeq.Completion.instPowCauchyNat = { pow := fun x n => Quotient.map (fun x => x ^ n) (_ : ∀ (x x_1 : CauSeq β abv), x ≈ x_1 → x ^ n ≈ x_1 ^ n) x }

source

ink

@[simp]

theorem CauSeq.Completion.mk_pow {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (n : ℕ) (f : CauSeq β abv) :

CauSeq.Completion.mk f ^ n = CauSeq.Completion.mk (f ^ n)

source

ink

instance CauSeq.Completion.instNatCastCauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

NatCast (CauSeq.Completion.Cauchy abv)

Equations

CauSeq.Completion.instNatCastCauchy = { natCast := fun n => CauSeq.Completion.mk ↑n }

source

ink

instance CauSeq.Completion.instIntCastCauchy {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

IntCast (CauSeq.Completion.Cauchy abv)

Equations

CauSeq.Completion.instIntCastCauchy = { intCast := fun n => CauSeq.Completion.mk ↑n }

source

ink

@[simp]

theorem CauSeq.Completion.ofRat_natCast {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (n : ℕ) :

CauSeq.Completion.ofRat ↑n = ↑n

source

ink

@[simp]

theorem CauSeq.Completion.ofRat_intCast {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (z : ℤ) :

CauSeq.Completion.ofRat ↑z = ↑z

source

ink

theorem CauSeq.Completion.ofRat_add {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) (y : β) :

CauSeq.Completion.ofRat (x + y) = CauSeq.Completion.ofRat x + CauSeq.Completion.ofRat y

source

ink

theorem CauSeq.Completion.ofRat_neg {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) :

CauSeq.Completion.ofRat (-x) = -CauSeq.Completion.ofRat x

source

ink

theorem CauSeq.Completion.ofRat_mul {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) (y : β) :

CauSeq.Completion.ofRat (x * y) = CauSeq.Completion.ofRat x * CauSeq.Completion.ofRat y

source

ink

instance CauSeq.Completion.Cauchy.ring {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

Ring (CauSeq.Completion.Cauchy abv)

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem CauSeq.Completion.ofRatRingHom_apply {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) :

↑CauSeq.Completion.ofRatRingHom x = CauSeq.Completion.ofRat x

source

ink

def CauSeq.Completion.ofRatRingHom {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] :

β →+* CauSeq.Completion.Cauchy abv

CauSeq.Completion.ofRat as a RingHom

Equations

One or more equations did not get rendered due to their size.

source

ink

theorem CauSeq.Completion.ofRat_sub {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) (y : β) :

CauSeq.Completion.ofRat (x - y) = CauSeq.Completion.ofRat x - CauSeq.Completion.ofRat y

source

ink

instance CauSeq.Completion.Cauchy.commRing {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : CommRing β] {abv : β → α} [inst : IsAbsoluteValue abv] :

CommRing (CauSeq.Completion.Cauchy abv)

Equations

One or more equations did not get rendered due to their size.

source

ink

instance CauSeq.Completion.instRatCastCauchyToRing {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] :

RatCast (CauSeq.Completion.Cauchy abv)

Equations

CauSeq.Completion.instRatCastCauchyToRing = { ratCast := fun q => CauSeq.Completion.ofRat ↑q }

source

ink

@[simp]

theorem CauSeq.Completion.ofRat_ratCast {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] (q : ℚ) :

CauSeq.Completion.ofRat ↑q = ↑q

source

ink

noncomputable instance CauSeq.Completion.instInvCauchyToRing {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] :

Inv (CauSeq.Completion.Cauchy abv)

Equations

One or more equations did not get rendered due to their size.

source

ink

theorem CauSeq.Completion.inv_zero {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] :

0⁻¹ = 0

source

ink

@[simp]

theorem CauSeq.Completion.inv_mk {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) :

(CauSeq.Completion.mk f)⁻¹ = CauSeq.Completion.mk (CauSeq.inv f hf)

source

ink

theorem CauSeq.Completion.cau_seq_zero_ne_one {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] :

¬0 ≈ 1

source

ink

theorem CauSeq.Completion.zero_ne_one {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] :

0 ≠ 1

source

ink

theorem CauSeq.Completion.inv_mul_cancel {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] {x : CauSeq.Completion.Cauchy abv} :

x ≠ 0 → x⁻¹ * x = 1

source

ink

theorem CauSeq.Completion.mul_inv_cancel {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] {x : CauSeq.Completion.Cauchy abv} :

x ≠ 0 → x * x⁻¹ = 1

source

ink

theorem CauSeq.Completion.ofRat_inv {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) :

CauSeq.Completion.ofRat x⁻¹ = (CauSeq.Completion.ofRat x)⁻¹

source

ink

noncomputable instance CauSeq.Completion.Cauchy.divisionRing {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] :

DivisionRing (CauSeq.Completion.Cauchy abv)

The Cauchy completion forms a division ring.

Equations

CauSeq.Completion.Cauchy.divisionRing = DivisionRing.mk zpowRec (_ : ∀ (x : CauSeq.Completion.Cauchy abv), x ≠ 0 → x * x⁻¹ = 1) (_ : 0⁻¹ = 0) (qsmulRec Rat.cast)

source

ink

theorem CauSeq.Completion.ofRat_div {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] (x : β) (y : β) :

CauSeq.Completion.ofRat (x / y) = CauSeq.Completion.ofRat x / CauSeq.Completion.ofRat y

source

ink

unsafe instance CauSeq.Completion.instReprCauchyToRing {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : DivisionRing β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : Repr β] :

Repr (CauSeq.Completion.Cauchy abv)

Show the first 10 items of a representative of this equivalence class of cauchy sequences.

The representative chosen is the one passed in the VM to quot.mk, so two cauchy sequences converging to the same number may be printed differently.

Equations

One or more equations did not get rendered due to their size.

source

ink

noncomputable instance CauSeq.Completion.Cauchy.field {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Field β] {abv : β → α} [inst : IsAbsoluteValue abv] :

Field (CauSeq.Completion.Cauchy abv)

The Cauchy completion forms a field.

Equations

One or more equations did not get rendered due to their size.

source

ink

class CauSeq.IsComplete {α : Type u_1} [inst : LinearOrderedField α] (β : Type u_2) [inst : Ring β] (abv : β → α) [inst : IsAbsoluteValue abv] :

Prop

Every Cauchy sequence has a limit.
isComplete : ∀ (s : CauSeq β abv), ∃ b, s ≈ CauSeq.const abv b

A class stating that a ring with an absolute value is complete, i.e. every Cauchy sequence has a limit.

Instances

source

ink

theorem CauSeq.complete {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] (s : CauSeq β abv) :

∃ b, s ≈ CauSeq.const abv b

source

ink

noncomputable def CauSeq.lim {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] (s : CauSeq β abv) :

The limit of a Cauchy sequence in a complete ring. Chosen non-computably.

Equations

CauSeq.lim s = Classical.choose (_ : ∃ b, s ≈ CauSeq.const abv b)

source

ink

theorem CauSeq.equiv_lim {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] (s : CauSeq β abv) :

s ≈ CauSeq.const abv (CauSeq.lim s)

source

ink

theorem CauSeq.eq_lim_of_const_equiv {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] {f : CauSeq β abv} {x : β} (h : CauSeq.const abv x ≈ f) :

x = CauSeq.lim f

source

ink

theorem CauSeq.lim_eq_of_equiv_const {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] {f : CauSeq β abv} {x : β} (h : f ≈ CauSeq.const abv x) :

CauSeq.lim f = x

source

ink

theorem CauSeq.lim_eq_lim_of_equiv {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] {f : CauSeq β abv} {g : CauSeq β abv} (h : f ≈ g) :

CauSeq.lim f = CauSeq.lim g

source

ink

@[simp]

theorem CauSeq.lim_const {α : Type u_2} [inst : LinearOrderedField α] {β : Type u_1} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] (x : β) :

CauSeq.lim (CauSeq.const abv x) = x

source

ink

theorem CauSeq.lim_add {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] (f : CauSeq β abv) (g : CauSeq β abv) :

CauSeq.lim f + CauSeq.lim g = CauSeq.lim (f + g)

source

ink

theorem CauSeq.lim_mul_lim {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] (f : CauSeq β abv) (g : CauSeq β abv) :

CauSeq.lim f * CauSeq.lim g = CauSeq.lim (f * g)

source

ink

theorem CauSeq.lim_mul {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] (f : CauSeq β abv) (x : β) :

CauSeq.lim f * x = CauSeq.lim (f * CauSeq.const abv x)

source

ink

theorem CauSeq.lim_neg {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] (f : CauSeq β abv) :

CauSeq.lim (-f) = -CauSeq.lim f

source

ink

theorem CauSeq.lim_eq_zero_iff {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Ring β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] (f : CauSeq β abv) :

CauSeq.lim f = 0 ↔ CauSeq.LimZero f

source

ink

theorem CauSeq.lim_inv {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst : Field β] {abv : β → α} [inst : IsAbsoluteValue abv] [inst : CauSeq.IsComplete β abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) :

CauSeq.lim (CauSeq.inv f hf) = (CauSeq.lim f)⁻¹

source

ink

theorem CauSeq.lim_le {α : Type u_1} [inst : LinearOrderedField α] [inst : CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α} (h : f ≤ CauSeq.const abs x) :

CauSeq.lim f ≤ x

source

ink

theorem CauSeq.le_lim {α : Type u_1} [inst : LinearOrderedField α] [inst : CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α} (h : CauSeq.const abs x ≤ f) :

x ≤ CauSeq.lim f

source

ink

theorem CauSeq.lt_lim {α : Type u_1} [inst : LinearOrderedField α] [inst : CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α} (h : CauSeq.const abs x < f) :

x < CauSeq.lim f

source

ink

theorem CauSeq.lim_lt {α : Type u_1} [inst : LinearOrderedField α] [inst : CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α} (h : f < CauSeq.const abs x) :

CauSeq.lim f < x