Email Gateway (Aug 22 2022 at 20:49): Email Gateway (Aug 22 2022 at 20:49):From: Peter Lammich <lammich@in.tum.de>
Hi,
the second lemma named "Inf_Sup" hides the first one, making it only
accessible by its (tedious to write) long name. Can we rename one of
these lemmas?
Email Gateway (Aug 22 2022 at 20:49):From: Tobias Nipkow <nipkow@in.tum.de>
The first one could/should be called Inf_eq_Sup.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 20:50):From: Viorel Preoteasa <viorel.preoteasa@gmail.com>
I guess that I am responsible for introducing the second lemma, and
there is also the dual version.
Probably changing Complete_Lattices.complete_distrib_lattice_class.Inf_Sup
to Complete_Lattices.complete_distrib_lattice_class.Inf_Sup_distrib
would be best as it would use the same pattern as inf_sup_distrib.
Viorel
Last updated: Apr 25 2024 at 04:18 UTC