Re: [isabelle] Redundant Information?



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. 

Larry

> 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 MHonArc.