# [isabelle] Redundant Information?

Hello,
In some libraries in Isabelle/HOL I saw the following structure:
proposition uniform_limit_iff:
"uniform_limit S f l F ⟷ (∀e>0. ∀⇩F n in F. ∀x∈S. dist (f n x) (l x) < e)"
lemma uniform_limitD:
"uniform_limit S f l F ⟹ e > 0 ⟹ ∀⇩F n in F. ∀x∈S. dist (f n x) (l x) < e"
lemma uniform_limitI:
"(⋀e. e > 0 ⟹ ∀⇩F n in F. ∀x∈S. dist (f n x) (l x) < e) ⟹ uniform_limit S
f l F"
The disadvantage of this approach is that it increases the search space of
lemmas for automatic reasoning tools. My questions are the following ones:
a) Is there any advantage in including the equivalence A ⟷ B as a lemma,
when we already have both A ⟹ B and B ⟹ A as lemmas?
b) Is there any advantage in including both A ⟹ B and B ⟹ A as lemmas, when
we already have the equivalence A ⟷ B as a lemma?
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"
Kind Regards,
José M.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*