On 2017-08-24 23:25, Manuel Eberl wrote:
Purely out of interest: Does this also hold for filters?
Manuel
Do filters form a complete lattice? It seems that a filter of a lattice
should be nonempty.
I think that this condition would prevent the set of filters to be a
lattice.
If empty set
Dear Christian,
They are useful, I have added them (and slightly modified the names):
http://isabelle.in.tum.de/repos/isabelle/rev/5df7a346f07b
Thanks
Tobias
On 25/08/2017 06:55, Christian Sternagel wrote:
Dear list,
maybe the following results about "lex" are worthwhile to add to the
Am 24.08.2017 um 22:39 schrieb Manuel Eberl:
> On 2017-08-24 17:34, Florian Haftmann wrote:
>> I would still appreciate if someone would take the comment »Deviates
>> from the definition given in the library in number theory« as a starting
>> point to reconcile that definition with
Dear Florian,
For the final record:
Concerning \mu and \nu, I am currently investigating whether an import
swap could re-establish the situation known from Isabelle2016-1
see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1
I had overlooked that \mu and \nu are global constants
I have investigated the possibility of replacing the existing
complete_distrib_lattice with the stronger version.
Here are the problems:
1. The new class needs Hilbert choice in few places: proving the dual
of the distributivity property, proving the set and fun instantiations,
and proving
