calc lt

Stream: new members

[Iocta]

What is going wrong in the last line?

import data.real.basic


def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

example (u l) : seq_limit u l ↔
 ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε :=
begin
apply iff.intro,
{
  unfold seq_limit,
  intros h ε ε_pos,
  cases h (ε/2) (by linarith) with N hN,
  use N,
  intros n hn,
  specialize hN n hn,
  calc
  | u n - l | ≤ ε / 2 : hN
  ... < ε : by linarith
},
{
intros h ε ε_pos,
cases h ε (by linarith) with N hN,
use N,
intros n hn,
specialize hN n hn,
calc
| u n - l | < ε : hN
... ≤ ε : by apply le_of_lt
},
end

invalid type ascription, term has type
  |u n - l| < ε
but is expected to have type
  |u n - l| ≤ ε
state:
u : ℕ → ℝ,
l : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |u n - l| < ε),
ε : ℝ,
ε_pos : ε > 0,
N n : ℕ,
hn : n ≥ N,
hN : |u n - l| < ε
⊢ |u n - l| ≤ ε

[Bryan Gin-ge Chen]

I had to mess with your code to get it to work. In particular, either the notation line was missing or you were missing an import:

import data.real.basic

notation `|` x `|` := abs x

def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

example (u l) : seq_limit u l ↔
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε :=
begin
  apply iff.intro,
  { unfold seq_limit,
    intros h ε ε_pos,
    cases h (ε/2) (by linarith) with N hN,
    use N,
    intros n hn,
    specialize hN n hn,
    calc
    | u n - l | ≤ ε / 2 : hN
    ... < ε : by linarith },
  { intros h ε ε_pos,
    cases h ε (by linarith) with N hN,
    use N,
    intros n hn,
    specialize hN n hn,
    exact le_of_lt hN, },
end

Your original calc strategy for closing the goal won't work because the first step shows that |u n - l| ≤ ε and then on the next line you have to somehow show that ε < ε to finish. The error message is definitely pretty confusing here.

[Iocta]

Ah I see, that makes sense