Re: [isabelle] Redundant Information?
- To: José Manuel Rodríguez Caballero <josephcmac at gmail.com>
- Subject: Re: [isabelle] Redundant Information?
- From: Lawrence Paulson <lp15 at cam.ac.uk>
- Date: Mon, 22 Jul 2019 11:38:26 +0100
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <CAA8xVUgxQ=HqRj3=k5x+x_Y7C_=5NS1ugFe0XzJKLC0Atmmn0Q@mail.gmail.com>
- References: <CAA8xVUgxQ=HqRj3=k5x+x_Y7C_=5NS1ugFe0XzJKLC0Atmmn0Q@mail.gmail.com>
In this case it’s surely significant that two notions of limit — one based on traditional epsilon-delta reasoning and the other on nonstandard analysis derived from ultrafilters — are equivalent.
> On 22 Jul 2019, at 08:22, José Manuel Rodríguez Caballero <josephcmac at gmail.com> wrote:
> c) Is there any case when it is useful to have two definitions A and B,
> even if we have the fact A ⟷ B? The typical example is:
> theorem LIMSEQ_NSLIMSEQ_iff: "f ⇢ L ⟷ f ⇢⇩N⇩S L"
This archive was generated by a fusion of
Pipermail (Mailman edition) and