Email Gateway (Aug 18 2022 at 17:34): Email Gateway (Aug 18 2022 at 17:34):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello
I have the following lemma.
context some_algebra begin;
lemma lesseq_lesseq_r: "(a <= b) = lesseq_r a b";
proof -;
interpret A: semilattice_inf lesseq_r less_r inf_r;
by unfold_locales;
show "(a <= b) = lesseq_r a b";
apply (subst le_iff_inf);
apply (subst A.le_iff_inf);
The context some_algebra implies a semilattice_inf structure for <=.
Also step labeled by A
proves that we have a semilattice_inf for lesseq_r.
However the proof step apply (subst A.le_iff_inf) fails with Unknown
fact "A.le_iff_inf".
I would be grateful for any help.
Best regards,
Viorel
Last updated: Apr 26 2024 at 08:19 UTC