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. 


> On 22 Jul 2019, at 08:22, José Manuel Rodríguez Caballero <josephcmac at> 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.