# Zulip Chat Archive

## Stream: maths

### Topic: Link between sequential and epsilon/delta versions

#### Ryan Lahfa (Apr 03 2020 at 19:04):

In real analysis, we often encounter sequential version of usual epsilon/delta definitions.

For example, sequential continuity, sequential uniform continuity, accumulation point of a set/sequence, inf/sup.

I have multiple questions Lean and non-Lean ones:

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?

(2) It looks like that the equivalence theorem between a sequential version and an epsilon/delta one is also independent of the concept and relies more on the form of the definition rather than on its contents, so, we should be able to produce the equivalence theorem given just a general version of such definitions, right? (under some assumption of choice for sequential → epsilon/delta).

(3) Is this something I could formalize in Lean? Would it be better to go for a type class in such cases?

Maybe, this question is not very relevant because it's impossible to have a general form of sequential version of definitions or things like that.

To give precise examples, here are definitions:

Accumulation point $a$ of a sequence $x$:

Epsilon/Delta: $\forall \varepsilon > 0, \forall n \geq 0, \exists N \geq n, \lvert x_n - a\rvert < \varepsilon$

Sequence form: $\exists y \in x(\mathbb{N})^{\mathbb{N}}, \lim_{n \to +\infty} y_n = a$

Sup:

We say that $a = \sup A$ if:

Epsilon/Delta: $\forall \varepsilon > 0, \exists x \in A, a - \varepsilon < x \leq a$

Sequence form: $\exists y \in A^{\mathbb{N}}, \lim_{n \to +\infty} y_n = a$

Continuity:

We say that $f : A \to B$ is continuous at $x \in A$ if:

Epsilon/delta: $\forall \varepsilon > 0, \exists \delta > 0, \forall y \in A, \lvert x - y \rvert \leq \delta \implies \lvert f(x) - f(y) \rvert \leq \varepsilon$

Sequence form: $\forall x \in A^{\mathbb{N}}, \left(\lim_{n \to +\infty} x_n = x\right) \implies \left(\lim_{n \to +\infty} f(x_n) = f(x)\right)$

#### Mario Carneiro (Apr 03 2020 at 19:35):

Filters are the unifying abstraction here

#### Mario Carneiro (Apr 03 2020 at 19:37):

In general topological spaces, sequential versions of many concepts exist and are different from the usual ones

#### Ryan Lahfa (Apr 03 2020 at 19:37):

Mario Carneiro said:

Filters are the unifying abstraction here

I wanted to avoid those :D… But I guess this is it

#### Mario Carneiro (Apr 03 2020 at 19:39):

Given a sequence there is a filter defined by "containing cofinitely many of the points of the sequence", and a limit of the filter is the same as a limit of the sequence

#### Mario Carneiro (Apr 03 2020 at 19:42):

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?

Actually, the logical manipulation you are doing to the definitions to get this is well known elsewhere as "skolemization", the interchanging of `\all x, \exists y, P x y`

with `\ex f, \forall x, P x (f x)`

#### Ryan Lahfa (Apr 03 2020 at 19:43):

Mario Carneiro said:

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?

Actually, the logical manipulation you are doing to the definitions to get this is well known elsewhere as "skolemization", the interchanging of

`\all x, \exists y, P x y`

with`\ex f, \forall x, P x (f x)`

Okay, I was remembering something in terms of "skolemization" and logic, but could not find what I needed. Thank you so much!

#### Mario Carneiro (Apr 03 2020 at 19:44):

although in order to make them sequences there is an additional step where you weaken the real number epsilon quantifier to an equivalent natural number quantifier

#### Mario Carneiro (Apr 03 2020 at 19:44):

(which is where the difference is in general, non first countable topological spaces)

#### Ryan Lahfa (Apr 03 2020 at 19:46):

Okay, it makes a lot of sense now, thank you!

#### Ryan Lahfa (Apr 03 2020 at 19:54):

Mario Carneiro said:

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?

Actually, the logical manipulation you are doing to the definitions to get this is well known elsewhere as "skolemization", the interchanging of

`\all x, \exists y, P x y`

with`\ex f, \forall x, P x (f x)`

BTW, is there any skolemization lemma in Lean?

#### Alex J. Best (Apr 03 2020 at 20:00):

`classical.skolem`

in core lean?

#### Kevin Buzzard (Apr 03 2020 at 20:04):

If you're formalising analysis in tactic mode you might never need to use terms such as this though

#### Ryan Lahfa (Apr 03 2020 at 20:08):

Kevin Buzzard said:

If you're formalising analysis in tactic mode you might never need to use terms such as this though

Why?

#### Ryan Lahfa (Apr 03 2020 at 20:09):

My problem is I often run into those dual definitions when I'm attempting to proof stuff.

And, when let's say I have a proof of having an accumulation point in an epsilon/delta-style, I'm not sure how to convert it into a sequence-style proof easily without writing a lot of machinery (?).

#### Patrick Massot (Apr 03 2020 at 20:21):

You shouldn't be afraid of filters. They are much nicer than epsiloneries.

#### Ryan Lahfa (Apr 03 2020 at 20:24):

Patrick Massot said:

You shouldn't be afraid of filters. They are much nicer than epsiloneries.

All the contrary, I love them; but I am not allowed to use them because of most students (and maybe non-topologists teachers) which do not understand them very well

But at the same time, I'm frustrated with repeating the same boring & technical proofs…

#### Kevin Buzzard (Apr 03 2020 at 20:51):

Ryan Lahfa said:

Kevin Buzzard said:

If you're formalising analysis in tactic mode you might never need to use terms such as this though

Why?

Because we have tactics like `choose`

.

#### Ryan Lahfa (Apr 03 2020 at 20:54):

Kevin Buzzard said:

Ryan Lahfa said:

Kevin Buzzard said:

If you're formalising analysis in tactic mode you might never need to use terms such as this though

Why?

Because we have tactics like

`choose`

.

Wow. That's awesome!

#### Ryan Lahfa (Apr 03 2020 at 21:53):

Though, I come back with an MWE because I didn't succeed to make `choose`

work well.

import data.set import data.set.finite import data.real.basic import data.finset import order.conditionally_complete_lattice noncomputable theory open_locale classical open set class metric_space (X : Type) := (d : X → X → ℝ) (d_pos : ∀ x y, d x y ≥ 0) (presep : ∀ x y, x=y → d x y = 0) (sep : ∀ x y, d x y = 0 → x = y) (sym : ∀ x y, d x y = d y x) (triangle : ∀ x y z, d x z ≤ d x y + d y z) variables {X:Type} [metric_space X] open metric_space def converge (x: ℕ → X) (l : X) := ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n)) < ε) lemma sup_is_a_cv_seq [conditionally_complete_linear_order X] (S: set X): S.nonempty → bdd_above S → ∃ (x: ℕ → X), (set.range x) ⊆ S ∧ converge x (Sup S) := begin intros hnn hbdd, end

Let's say I want to prove that `sup_is_a_cv_seq`

, so ideally, I should be able to reuse some parts of `mathlib`

, namely `cSup_intro`

I imagine and taking `ϵ = 1/n`

for all n ≥ 0, this way, I should be able to have this lemma easily w/o rewriting a lot of stuff, right?

#### Ryan Lahfa (Apr 03 2020 at 22:09):

Specifically, if I try to do this:

import data.set import data.set.finite import data.real.basic import data.finset import order.conditionally_complete_lattice noncomputable theory open_locale classical open set class metric_space (X : Type) := (d : X → X → ℝ) (d_pos : ∀ x y, d x y ≥ 0) (presep : ∀ x y, x=y → d x y = 0) (sep : ∀ x y, d x y = 0 → x = y) (sym : ∀ x y, d x y = d y x) (triangle : ∀ x y z, d x z ≤ d x y + d y z) variables {X:Type} [metric_space X] open metric_space def converge (x: ℕ → X) (l : X) := ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n)) < ε) lemma sup_is_a_cv_seq [conditionally_complete_linear_order X] (S: set X): S.nonempty → bdd_above S → ∃ (x: ℕ → X), (set.range x) ⊆ S ∧ converge x (Sup S) := begin intros hnn hbdd, have: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := sorry, have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x < 1/(N + 1) := sorry, choose x hrange h using this, use x, split, intros y hy, obtain ⟨ N, hN ⟩ := hy, rw ← hN, exact hrange N, intros ε hε, -- 1/(N + 1) ≤ eps -- 1/eps ≤ N + 1 -- 1/eps - 1 ≤ N -- use (floor(1/eps - 1) + 1) use (floor((1/ϵ) - 1) + 1), end

The `use`

won't work.

#### Ryan Lahfa (Apr 03 2020 at 22:09):

Because floor is in Z and I have to prove that the total value is in N, I guess.

#### Ryan Lahfa (Apr 03 2020 at 22:12):

Huh, no, the code provided uses a ϵ and the ε is not the same…

#### Ryan Lahfa (Apr 03 2020 at 22:16):

Wonder if it is my CPU or something, but:

import data.set import data.set.finite import data.real.basic import data.finset import order.conditionally_complete_lattice noncomputable theory open_locale classical open set class metric_space (X : Type) := (d : X → X → ℝ) (d_pos : ∀ x y, d x y ≥ 0) (presep : ∀ x y, x=y → d x y = 0) (sep : ∀ x y, d x y = 0 → x = y) (sym : ∀ x y, d x y = d y x) (triangle : ∀ x y z, d x z ≤ d x y + d y z) variables {X:Type} [metric_space X] open metric_space def converge (x: ℕ → X) (l : X) := ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n)) < ε) lemma sup_is_a_cv_seq [conditionally_complete_linear_order X] (S: set X): S.nonempty → bdd_above S → ∃ (x: ℕ → X), (set.range x) ⊆ S ∧ converge x (Sup S) := begin intros hnn hbdd, have: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := sorry, have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x < 1/(N + 1) := sorry, choose x hrange h using this, use x, split, intros y hy, obtain ⟨ N, hN ⟩ := hy, rw ← hN, exact hrange N, intros ε hε, -- 1/(N + 1) ≤ eps -- 1/eps ≤ N + 1 -- 1/eps - 1 ≤ N -- use (floor(1/eps - 1) + 1) set N₀ := (floor((1/ε) - 1) + 1), have N0_pos: N₀ ≥ 0 := sorry, -- lift N₀ to ℕ using N0_pos, use N₀, sorry, end

is taking a lot of time to compute.

#### Kevin Buzzard (Apr 03 2020 at 22:29):

`presep`

could be less clunkily expressed as `forall x, d x x = 0`

, and `d_pos`

follows from `triangle`

and `sym`

and `presep`

#### Ryan Lahfa (Apr 03 2020 at 22:30):

Kevin Buzzard said:

`presep`

could be less clunkily expressed as`forall x, d x x = 0`

, and`d_pos`

follows from`triangle`

and`sym`

and`presep`

Thank you!

#### Kevin Buzzard (Apr 03 2020 at 22:31):

I am concerned about your first `sorry`

#### Mario Carneiro (Apr 03 2020 at 22:31):

at the risk of pointing out the obvious, mathlib already has a definition of metric spaces

#### Kevin Buzzard (Apr 03 2020 at 22:31):

But what about a metric space which is also a conditionally complete linear order?

#### Kevin Buzzard (Apr 03 2020 at 22:31):

Because I am concerned that these two structures, the way you have set things up, are completely unrelated.

#### Ryan Lahfa (Apr 03 2020 at 22:32):

Mario Carneiro said:

at the risk of pointing out the obvious, mathlib already has a definition of metric spaces

I know, this is rather to have another metric space definition which does not use filters, but only standard sequences.

#### Mario Carneiro (Apr 03 2020 at 22:32):

but the definition doesn't say anything about sequences

#### Kevin Buzzard (Apr 03 2020 at 22:32):

For example I don't see any reason why `Sup S`

(which is defined using the complete linear order structure) should have anything to do with `converge`

(which is defined using he metric space)

#### Ryan Lahfa (Apr 03 2020 at 22:32):

Kevin Buzzard said:

Because I am concerned that these two structures, the way you have set things up, are completely unrelated.

Yes, I definitely feel super wrong about this too. But in order to talk about Sup, I need some structure where bounded above gives me a sup.

#### Kevin Buzzard (Apr 03 2020 at 22:33):

Sure, but you haven't glued your two choices of structure together

#### Ryan Lahfa (Apr 03 2020 at 22:33):

Kevin Buzzard said:

For example I don't see any reason why

`Sup S`

(which is defined using the complete linear order structure) should have anything to do with`converge`

(which is defined using he metric space)

Wouldn't cSup_intro give me the first sorry?

#### Kevin Buzzard (Apr 03 2020 at 22:33):

You can't prove any theorem relating sups to distances here

#### Ryan Lahfa (Apr 03 2020 at 22:33):

Mario Carneiro said:

but the definition doesn't say anything about sequences

Of metric spaces?

#### Ryan Lahfa (Apr 03 2020 at 22:33):

Kevin Buzzard said:

You can't prove any theorem relating sups to distances here

I see what you mean, right.

#### Mario Carneiro (Apr 03 2020 at 22:34):

I think you want to know that the topology is `orderable`

#### Kevin Buzzard (Apr 03 2020 at 22:34):

You have currently written "Let $X$ be a metric space. Assume also that $X$ has a total order, which is completely unrelated to the metric space structure. Then..."

#### Mario Carneiro (Apr 03 2020 at 22:34):

but that requires the topology of the metric space, so at that point you are better off using the mathlib definition

#### Mario Carneiro (Apr 03 2020 at 22:35):

You can probably recast it in terms of compatibility directly, something like "intervals contain open balls and vice versa"

#### Ryan Lahfa (Apr 03 2020 at 22:39):

Let's assume I want to prove this only for $\mathbb{R}$ right now, so the first sorry is not a problem anymore, right? I can just remove the total orderable condition.

#### Ryan Lahfa (Apr 03 2020 at 22:41):

Okay, I see now why the first sorry was not feasible, indeed.

#### Kevin Buzzard (Apr 03 2020 at 22:51):

If you don't want to work with $\mathbb{R}$ directly you need to come up with some structure where the ideas you want to formalise are still true, and it sounds to me like you want the topology induced by the metric to equal the topology induced by the order.

#### Kevin Buzzard (Apr 03 2020 at 22:52):

So either you formalise what the topology induced by your metric is, or you use mathlib metric spaces where it's already there.

#### Ryan Lahfa (Apr 03 2020 at 22:53):

I'll directly work with $\mathbb{R}$ right now because I won't use this lemma for something else than $\mathbb{R}$.

After I succeed, I'll revisit it to improve it with the topology order condition rather.

#### Ryan Lahfa (Apr 03 2020 at 22:53):

My whole code becomes now:

import data.set import data.set.finite import data.real.basic import data.finset import order.conditionally_complete_lattice noncomputable theory open_locale classical open set class metric_space (X : Type) := (d : X → X → ℝ) (d_pos : ∀ x y, d x y ≥ 0) (presep : ∀ x y, x = y → d x y = 0) (sep : ∀ x y, d x y = 0 → x = y) (sym : ∀ x y, d x y = d y x) (triangle : ∀ x y z, d x z ≤ d x y + d y z) variables {X:Type} [metric_space X] open metric_space instance real.metric_space : metric_space ℝ := { d := λx y, abs (x - y), d_pos := by simp [abs_nonneg], presep := begin simp, apply sub_eq_zero_of_eq end, sep := begin simp, apply eq_of_sub_eq_zero end, sym := assume x y, abs_sub _ _, triangle := assume x y z, abs_sub_le _ _ _ } theorem real.dist_eq (x y : ℝ) : d x y = abs (x - y) := rfl theorem real.dist_0_eq_abs (x : ℝ) : d x 0 = abs x := by simp [real.dist_eq] def converge (x: ℕ → X) (l : X) := ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n)) < ε) lemma sup_is_a_cv_seq (S: set ℝ): S.nonempty → bdd_above S → ∃ (x: ℕ → ℝ), (set.range x) ⊆ S ∧ converge x (Sup S) := begin intros hnn hbdd, have: ∀ ε > 0, ∃ x ∈ S, Sup S - x < ε := sorry, have: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := begin intros ε hε, obtain ⟨ x, hx, hs_lt ⟩ := this ε hε, use x, split, exact hx, rw real.dist_eq, apply abs_lt_of_lt_of_neg_lt, exact hs_lt, sorry, -- by definition of sup. end, have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x < 1/(N + 1) := sorry, choose x hrange h using this, use x, split, intros y hy, obtain ⟨ N, hN ⟩ := hy, rw ← hN, exact hrange N, intros ε hε, -- 1/(N + 1) ≤ eps -- 1/eps ≤ N + 1 -- 1/eps - 1 ≤ N lift floor(1/ε) to ℕ with N₀, use N₀, intros n hn, transitivity, exact h n, sorry, end

#### Kevin Buzzard (Apr 03 2020 at 22:54):

I can't find `orderable`

in mathlib by the way

#### Kevin Buzzard (Apr 03 2020 at 22:54):

Do you have a question or are you now OK to keep going?

#### Ryan Lahfa (Apr 03 2020 at 22:55):

I think I can now finish the proof by myself —but feel free if you see stupid things (except the fact I'm writing my own metric_space def which is only for the sake of exercise.)

#### Kevin Buzzard (Apr 03 2020 at 22:56):

Your proof looks just like the kind of proofs I was writing when I was learning.

#### Ryan Lahfa (Apr 03 2020 at 22:58):

I definitely abuse of `have`

because I'm trying to see how it works, but I clean up afterwards to have something more natural

#### Ryan Lahfa (Apr 03 2020 at 22:59):

Other than this, I think I might be using `obtain`

in a suboptimal way sometimes, and I'm not sure by what I should replace it

#### Ryan Lahfa (Apr 03 2020 at 23:00):

`transitivity`

is cool because it expresses 1:1 how I think, but those meta variables are not good I guess ; also, it does not work when I want to do: a ≤ b < c — I don't know what good replacement there would be for this? (I could chain the right lemmas given enough time, but it's somewhat annoying)

#### Kevin Buzzard (Apr 03 2020 at 23:00):

`lt_of_le_of_lt`

#### Ryan Lahfa (Apr 03 2020 at 23:01):

I should try to have the confidence to write those directly as they're so natural…

#### Mario Carneiro (Apr 03 2020 at 23:09):

it's actually `order_topology`

#### Mario Carneiro (Apr 03 2020 at 23:11):

I think the names changed at some point; there is `order_topology`

and `order_closed_topology`

now

#### Reid Barton (Apr 03 2020 at 23:13):

I also distinctly remember something about `orderable`

#### Scott Morrison (Apr 04 2020 at 02:27):

You can also use `calc`

blocks instead of `transitivity`

, or having the confidence to write `lt_of_le_of_lt`

.

#### Scott Morrison (Apr 04 2020 at 02:28):

`calc`

blocks also have the advantage of readability (as long as the proof terms on each line stay succinct).

#### Patrick Massot (Apr 04 2020 at 09:14):

Ryan, do you know that transitivity can take an argument instantiating the meta-variable you complain about?

#### Patrick Massot (Apr 04 2020 at 09:15):

I still agree with Scott that you should probably be using more calc blocks. `linarith`

can also get rid of all this as long as you state the relevant fact before, or pass them to linarith.

#### Ryan Lahfa (Apr 04 2020 at 09:16):

@Patrick Massot I didn't know and I should have tried, I assumed that `transitivity`

didn't take any argument, thanks.

#### Patrick Massot (Apr 04 2020 at 09:16):

Your lemma `sup_is_a_cv_seq`

was the end goal of my Lean L1 course last year.

#### Ryan Lahfa (Apr 04 2020 at 09:16):

Patrick Massot said:

I still agree with Scott that you should probably be using more calc blocks.

`linarith`

can also get rid of all this as long as you state the relevant fact before, or pass them to linarith.

I'll give a try to `calc`

blocks, they look like more natural to me.

#### Patrick Massot (Apr 04 2020 at 09:17):

But you are not approaching it in the right Lean mindset. You need to write the proof on paper, and collect all the « obvious facts » used in the proof. Them write lemmas about those obvious facts.

#### Kenny Lau (Apr 04 2020 at 09:17):

I don't like `(set.range x) ⊆ S`

because it is harder to prove and use than `\forall n, x n \in S`

#### Patrick Massot (Apr 04 2020 at 09:17):

Yes, I wanted to write this also.

#### Ryan Lahfa (Apr 04 2020 at 09:18):

Patrick Massot said:

Your lemma

`sup_is_a_cv_seq`

was the end goal of my Lean L1 course last year.

Oh wow, ideally, I'd like to generalize it to orderable topologies, like I'd been advised by @Mario Carneiro (behind this, I'm proving the classical Bolzano-Weierstrass)

#### Patrick Massot (Apr 04 2020 at 09:18):

`set.range`

and `set.image`

are evil. They look nice on paper because you automatically do the required bureaucracy in your head without noticing.

#### Patrick Massot (Apr 04 2020 at 09:19):

Sorry, I meant "of the exam of my Lean L1 course".

#### Ryan Lahfa (Apr 04 2020 at 09:19):

Patrick Massot said:

`set.range`

and`set.image`

are evil. They look nice on paper because you automatically do the required bureaucracy in your head without noticing.

Kenny Lau said:

I don't like

`(set.range x) ⊆ S`

because it is harder to prove and use than`\forall n, x n \in S`

Alright, but stating `\forall n, x n \in S`

looks like a bit weird when in reality what I want to express is that the image of the sequence is a subset of S

#### Patrick Massot (Apr 04 2020 at 09:19):

I forgot part of the sentence.

#### Ryan Lahfa (Apr 04 2020 at 09:19):

Patrick Massot said:

I forgot part of the sentence.

Patrick Massot said:

Sorry, I meant "of the exam of my Lean L1 course".

Ah! Is it available somewhere? I'm quite interested into this!

#### Patrick Massot (Apr 04 2020 at 09:19):

No, you want to express that the sequence takes values in S.

#### Patrick Massot (Apr 04 2020 at 09:20):

You would never say "the image of the sequence is a subset of S".

#### Ryan Lahfa (Apr 04 2020 at 09:20):

Indeed, I agree

#### Ryan Lahfa (Apr 04 2020 at 09:21):

But I'd just write $(x_n)_n \in S^{\mathbb{N}}$

#### Kenny Lau (Apr 04 2020 at 09:22):

but whenever you prove / use this sentence you always prove that $x_n \in S \forall n$

#### Patrick Massot (Apr 04 2020 at 09:23):

Ryan Lahfa said:

But I'd just write $(x_n)_n \in S^{\mathbb{N}}$

You shouldn't. Really.

#### Ryan Lahfa (Apr 04 2020 at 09:24):

Patrick Massot said:

Ryan Lahfa said:

But I'd just write $(x_n)_n \in S^{\mathbb{N}}$

You shouldn't. Really.

What would you advise to write?

#### Patrick Massot (Apr 04 2020 at 09:26):

Anyway, you should have lemma saying `∀ ε > 0, ∃ x ∈ S, Sup S - ε < x`

outside from your main proof. And then the same with 1/(N+1) instead of ε.

#### Ryan Lahfa (Apr 04 2020 at 09:28):

Patrick Massot said:

Anyway, you should have lemma saying

`∀ ε > 0, ∃ x ∈ S, Sup S - ε < x`

outside from your main proof. And then the same with 1/(N+1) instead of ε.

Yes, I was planning to extract those as they're looking like lemmas on themselves.

#### Patrick Massot (Apr 04 2020 at 09:28):

And a lemma saying that if for all n, `d (x n) l < 1/(N+1)`

then `x`

converges to `l`

.

#### Patrick Massot (Apr 04 2020 at 09:29):

Because these all lemmas that are "obvious" when you have already reached the point where you want to prove this Sup thing.

#### Patrick Massot (Apr 04 2020 at 09:29):

So you don't want to be proving them in the middle of this proof.

#### Patrick Massot (Apr 04 2020 at 09:29):

You wouldn't do that on paper and you wouldn't do that in Lean.

#### Patrick Massot (Apr 04 2020 at 09:30):

And of course a lemma saying that 1/(N+1) is less than any epsilon for N large enough

#### Ryan Lahfa (Apr 04 2020 at 09:33):

Definitely.

#### Ryan Lahfa (Apr 04 2020 at 09:33):

Would `one_div_lt_epsilon`

be a right name for the last lemma?

#### Ryan Lahfa (Apr 04 2020 at 09:34):

For `forall n, d (x n) l < 1/(N + 1) → converge x l`

, I'm not sure how to call it except `convergence_aux_1`

#### Patrick Massot (Apr 04 2020 at 09:35):

`converge_of_dist_lt_one_div_succ`

?

#### Kenny Lau (Apr 04 2020 at 09:35):

`converge_of_d_lt`

#### Ryan Lahfa (Apr 04 2020 at 13:47):

I tried to take into account most of your advice and came back with this:

import data.set import data.set.finite import data.real.basic import data.finset import order.conditionally_complete_lattice noncomputable theory open_locale classical open set class metric_space (X : Type) := (d : X → X → ℝ) (d_pos : ∀ x y, d x y ≥ 0) (presep : ∀ x y, x = y → d x y = 0) (sep : ∀ x y, d x y = 0 → x = y) (sym : ∀ x y, d x y = d y x) (triangle : ∀ x y z, d x z ≤ d x y + d y z) variables {X:Type} [metric_space X] open metric_space instance real.metric_space : metric_space ℝ := { d := λx y, abs (x - y), d_pos := by simp [abs_nonneg], presep := begin simp, apply sub_eq_zero_of_eq end, sep := begin simp, apply eq_of_sub_eq_zero end, sym := assume x y, abs_sub _ _, triangle := assume x y z, abs_sub_le _ _ _ } theorem real.dist_eq (x y : ℝ) : d x y = abs (x - y) := rfl theorem real.dist_0_eq_abs (x : ℝ) : d x 0 = abs x := by simp [real.dist_eq] def converge (x: ℕ → X) (l : X) := ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n)) < ε) lemma real.sup_sub_lt_eps {S: set ℝ}: ∀ ε > 0, ∃ x ∈ S, Sup S - x < ε := sorry lemma real.sup_dist_lt_eps {S: set ℝ}: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := begin intros ε hε, obtain ⟨ x, hx, hs_lt ⟩ := real.sup_sub_lt_eps ε hε, use x, split, exact hx, rw real.dist_eq, apply abs_lt_of_lt_of_neg_lt, exact hs_lt, sorry, end lemma converge_of_dist_lt_one_div_succ {x: ℕ → ℝ} {l: ℝ}: (∀ n, d l (x n) ≤ 1 / (n + 1)) → converge x l := begin intro H, intros ε hε, obtain ⟨ N, hN ⟩ := exists_nat_one_div_lt hε, use N, intros n hn, calc d l (x n) ≤ 1 / (n + 1) : H n ... ≤ 1 / (N + 1) : nat.one_div_le_one_div hn ... < ε : hN end lemma sup_is_a_cv_seq (S: set ℝ): S.nonempty → bdd_above S → ∃ (x: ℕ → ℝ), (∀ n, x n ∈ S) ∧ converge x (Sup S) := begin intros hnn hbdd, have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x < 1/(N + 1) := begin intro N, apply real.sup_dist_lt_eps, apply nat.one_div_pos_of_nat, end, choose x hrange h using this, use x, split, exact hrange, exact converge_of_dist_lt_one_div_succ h, -- this line should work (?) end

But, I have some issue regarding the types, here is the state at the last step:

type mismatch at application converge_of_dist_lt_one_div_succ h term h has type ∀ (N : ℕ), d (Sup S) (x N) < 1 / (↑N + 1) but is expected to have type ∀ (n : ℕ), d (Sup S) (x n) ≤ 1 / (↑n + 1) state: S : set ℝ, hnn : set.nonempty S, hbdd : bdd_above S, x : ℕ → ℝ, hrange : ∀ (N : ℕ), x N ∈ S, h : ∀ (N : ℕ), d (Sup S) (x N) < 1 / (↑N + 1) ⊢ converge x (Sup S)

I'm not sure what is actually different except some typeclasses, I tried to print those with `set_option pp.all true`

but got lost as there were a huge amount of those.

#### Kevin Buzzard (Apr 04 2020 at 13:49):

You have a < in one and a <=in the other

#### Ryan Lahfa (Apr 04 2020 at 13:49):

Thanks…

#### Ryan Lahfa (Apr 04 2020 at 13:51):

@Kevin Buzzard Is there a way to apply `le_of_lt`

in this part:

have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x ≤ 1/(N + 1) := begin intro N, apply le_of_lt, -- won't work because of exists apply real.sup_dist_lt_eps, apply nat.one_div_pos_of_nat, end,

?

#### Kevin Buzzard (Apr 04 2020 at 13:56):

Instead of `apply`

use `convert`

maybe. What is the type of real.sup_dist_lt_pos?

#### Ryan Lahfa (Apr 04 2020 at 13:56):

Kevin Buzzard said:

Instead of

`apply`

use`convert`

maybe. What is the type of real.sup_dist_lt_pos?

`lemma real.sup_dist_lt_eps {S: set ℝ}: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := begin`

#### Kevin Buzzard (Apr 04 2020 at 13:57):

Make a term which starts with an exists from that term and convert it

#### Kevin Buzzard (Apr 04 2020 at 13:58):

Ie supply the correct epsilon

#### Kevin Buzzard (Apr 04 2020 at 13:58):

Hmm this still won't work

#### Reid Barton (Apr 04 2020 at 13:58):

right, it won't work because `le_of_lt`

is not an equality

#### Ryan Lahfa (Apr 04 2020 at 13:59):

I tried this: `convert real.sup_dist_lt_eps (1 / (N + 1)) (nat.one_div_pos_of_nat),`

#### Kevin Buzzard (Apr 04 2020 at 13:59):

Well just do cases on the term to get to an epsilon

#### Kevin Buzzard (Apr 04 2020 at 13:59):

Convert won't work

#### Reid Barton (Apr 04 2020 at 13:59):

You need to know if $P(x) \implies Q(x)$ for all x, then $(\exists x, P(x)) \implies (\exists x, Q(x))$ and we don't have a general framework for that

#### Reid Barton (Apr 04 2020 at 13:59):

If it was $=$ and not $\implies$ then you could use convert or conv or whatever.

#### Kevin Buzzard (Apr 04 2020 at 14:00):

Do cases on the term you make with the exists and use that x

#### Kevin Buzzard (Apr 04 2020 at 14:02):

Or just apply the logic lemma. Presumably it's in logic.basic?

#### Ryan Lahfa (Apr 04 2020 at 14:02):

Kevin Buzzard said:

Well just do cases on the term to get to an epsilon

Is this something like this: `cases (real.sup_dist_lt_eps (1 / (N + 1)) (nat.one_div_pos_of_nat)) with x hx,`

often?

#### Kevin Buzzard (Apr 04 2020 at 14:03):

If you got an x and an hx that looks good then yes. You might be better off with rcases though

#### Kevin Buzzard (Apr 04 2020 at 14:04):

Because you want to extract x in S and not just x

#### Ryan Lahfa (Apr 04 2020 at 14:04):

Is there a preference between rcases and obtain?

#### Ryan Lahfa (Apr 04 2020 at 14:04):

Because I often use obtain to extract arbitrary complex constructors

#### Kevin Buzzard (Apr 04 2020 at 14:05):

Obtain is best

#### Ryan Lahfa (Apr 04 2020 at 14:05):

This works:

have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x ≤ 1/(N + 1) := begin intro N, obtain ⟨ x, hrange, hsup ⟩ := (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat)), use x, split, exact hrange, apply le_of_lt, exact hsup, end,

anyway

#### Kevin Buzzard (Apr 04 2020 at 14:05):

I always forget about it because it's relatively new

#### Ryan Lahfa (Apr 04 2020 at 14:05):

Thanks!

#### Kevin Buzzard (Apr 04 2020 at 14:06):

Now can you write it in pure term mode?

#### Kevin Buzzard (Apr 04 2020 at 14:06):

lambda instead of intro etc?

#### Kevin Buzzard (Apr 04 2020 at 14:07):

There are no serious tactics in your code so you don't need tactic mode at all

#### Kevin Buzzard (Apr 04 2020 at 14:07):

Obtain becomes let ... in

#### Kevin Buzzard (Apr 04 2020 at 14:07):

Split is pointy brackets

#### Kevin Buzzard (Apr 04 2020 at 14:07):

And exact can be removed completely

#### Ryan Lahfa (Apr 04 2020 at 14:08):

I started like this: ```
λ N,
let ⟨ x, hrange, hsup ⟩ in (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat)),
```

#### Ryan Lahfa (Apr 04 2020 at 14:08):

But it is complaining about the syntax — I guess I'm doing something wrong

#### Ryan Lahfa (Apr 04 2020 at 14:09):

Huh, yes `let x := t in s`

#### Patrick Massot (Apr 04 2020 at 14:09):

Your use of `obtain`

make it completely equivalent to `rcases`

. This is fine, but you should know the added value of `obtain`

is you can write the expected type upfront.

#### Patrick Massot (Apr 04 2020 at 14:10):

In your case that would be purely for readability purposes.

#### Ryan Lahfa (Apr 04 2020 at 14:11):

Patrick Massot said:

Your use of

`obtain`

make it completely equivalent to`rcases`

. This is fine, but you should know the added value of`obtain`

is you can write the expected type upfront.

I see, I can do `obtain <pattern>: type := …`

and I can omit `<pattern>`

?

#### Ryan Lahfa (Apr 04 2020 at 14:12):

@Kevin Buzzard I'm not sure how to replace the `use x;`

(also is there any docs for the commands for the pointy brackets, etc. ?)

#### Patrick Massot (Apr 04 2020 at 14:13):

You can do a lot of things:

obtain ⟨x, hx⟩ : ∃ x, P x, { long proof... }, obtain ⟨x, hx⟩ : ∃ x, P x := proof_term, obtain ⟨x, hx⟩ : ∃ x, P x, from proof_term,

#### Patrick Massot (Apr 04 2020 at 14:14):

Only the first case really needs obtain rather than rcases. But all are more readable than rcases

#### Patrick Massot (Apr 04 2020 at 14:14):

And of course you can get the same with `have`

+ `rcases`

but you'd get tired of this pretty quickly.

#### Ryan Lahfa (Apr 04 2020 at 14:16):

Makes sense, is there any docs to write tactics? I'm understanding more and more how to compose all of this and I'm interested in how it works

#### Kevin Buzzard (Apr 04 2020 at 14:23):

Beginning tactic writing is covered in a doc which Patrick wrote in the docs directory of mathlib

#### Ryan Lahfa (Apr 04 2020 at 14:28):

Now I'm this far:

have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x ≤ 1/(N + 1) := λ N, let ⟨ x, ha, hb ⟩ := (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat)) in exists.intro x (λ hp, and.intro (...) (...) ),

Is it expected that Lean VSCode cannot print the current state in term mode?

#### Kevin Buzzard (Apr 04 2020 at 14:29):

Use X is just <X,_> with the right brackets

#### Bhavik Mehta (Apr 04 2020 at 14:29):

By the way, can we make VSCode highlight obtain (and set) the same way as have (and let)?

#### Reid Barton (Apr 04 2020 at 14:30):

Use `_`

where you have `(...)`

, and then hover over it, or something (I use emacs, but I assume vscode can do this too)

#### Gabriel Ebner (Apr 04 2020 at 14:31):

@Bhavik Mehta Feel free to PR a change to this file: https://github.com/leanprover/vscode-lean/blob/9a4400a1f3db57d0a25c1944812b0c2dc9ff2141/syntaxes/lean.json#L35 But I wouldn't highlight `set`

: this occurs often as a non-tactic, e.g. in `set α`

.

#### Ryan Lahfa (Apr 04 2020 at 14:31):

Indeed, it works when I use `_`

, now I have this state:

context: S : set ℝ, hnn : set.nonempty S, hbdd : bdd_above S, N : ℕ, _let_match : (∃ (x : ℝ) (H : x ∈ S), d (Sup S) x < 1 / (↑N + 1)) → (∃ (x : ℝ) (H : x ∈ S), d (Sup S) x ≤ 1 / (↑N + 1)), x : ℝ, ha : x ∈ S, hb : d (Sup S) x < 1 / (↑N + 1) ⊢ ∃ (H : x ∈ S), d (Sup S) x ≤ 1 / (↑N + 1)

But the `exists`

in front of this is strange? I'm not sure how I can combine ha/hb to finish

#### Bhavik Mehta (Apr 04 2020 at 14:32):

Gabriel Ebner said:

Bhavik Mehta Feel free to PR a change to this file: https://github.com/leanprover/vscode-lean/blob/9a4400a1f3db57d0a25c1944812b0c2dc9ff2141/syntaxes/lean.json#L35 But I wouldn't highlight

`set`

: this occurs often as a non-tactic, e.g. in`set α`

.

Thanks! Ah yeah good point

#### Ryan Lahfa (Apr 04 2020 at 14:32):

have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x ≤ 1/(N + 1) := λ N, let ⟨ x, ha, hb ⟩ := (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat)) in ⟨ x, ⟨ ha, le_of_lt hb ⟩ ⟩,

This seems to work!

#### Ryan Lahfa (Apr 04 2020 at 14:34):

Thank you for the tip! I have seen symbols like `▸ `

, what does that mean? I see it in `mathlib`

sometimes, but I didn't find any docs on it

#### Reid Barton (Apr 04 2020 at 14:34):

ah, the dreaded "stupid triangle"

#### Patrick Massot (Apr 04 2020 at 14:36):

also known by its full name as the dreaded "I'm-sorry-but-I-don't-know-the-expected-type triangle".

#### Reid Barton (Apr 04 2020 at 14:37):

if `p : P a`

and `e : a = b`

then `e ▸ p : P b`

, except it basically never manages to work out what `P`

should be

#### Reid Barton (Apr 04 2020 at 14:37):

it's like a term-mode version of `rw`

that rarely works

#### Ryan Lahfa (Apr 04 2020 at 14:37):

Oh okay

#### Patrick Massot (Apr 04 2020 at 14:38):

You get extra credit when you manage to use it in a proof.

#### Ryan Lahfa (Apr 04 2020 at 14:38):

Hahahaha

#### Kevin Buzzard (Apr 04 2020 at 14:44):

Good job for getting the term!

#### Kevin Buzzard (Apr 04 2020 at 14:46):

One thing to remember about the stupid triangle is that in contrast to tactic mode it has to be told all inputs , ie rw add_comm works but with the triangle you might have to put add_comm a b

Last updated: May 10 2021 at 08:14 UTC