Email Gateway (Aug 18 2022 at 13:50): Email Gateway (Aug 18 2022 at 13:50):From: Andrei Popescu <uuomul@yahoo.com>
Hello,
I was wondering if one [has proved]/[can prove] in Isabelle/HOL that any infinite type 'a has an injection from 'a * 'a to 'a. Namely:
definition
injective :: "('a => 'b) => bool"
where
"injective f == ALL x x'. f x = f x' --> x = x'"
lemma
"~ finite(UNIV::'a set) ==> EX (f :: ('a * 'a) => 'a). injective f"
(At least for well-ordered 'a should be provable. Related question: can one prove (similarly to the case of ZF+Choice) that any type can be well-ordered? Is there any theory of ordinals developed in Isabelle/HOL?)
Thank you in advance,
Andrei Popescu
Email Gateway (Aug 18 2022 at 13:51):From: Tobias Nipkow <nipkow@in.tum.de>
Andrei Popescu wrote:
(At least for well-ordered 'a should be provable. Related question: can one prove (similarly to the case of ZF+Choice) that any type can be well-ordered?
Yes. See Library/Zorn.thy
Is there any theory of ordinals developed in Isabelle/HOL?)
Yes. See http://afp.sourceforge.net/entries/Ordinal.shtml
Tobias
Thank you in advance,
Andrei Popescu
Email Gateway (Aug 18 2022 at 13:51):From: Tobias Nipkow <nipkow@in.tum.de>
Andrei Popescu wrote:
Hello,
I was wondering if one [has proved]/[can prove] in Isabelle/HOL that any infinite type 'a has an injection from 'a * 'a to 'a. Namely:
definition
injective :: "('a => 'b) => bool"
where
"injective f == ALL x x'. f x = f x' --> x = x'"
A grep for "injective" will quickly show you that it already exists
under the name "inj" (and the related "inj_on").
Regards
Tobias
lemma
"~ finite(UNIV::'a set) ==> EX (f :: ('a * 'a) => 'a). injective f"(At least for well-ordered 'a should be provable. Related question: can one prove (similarly to the case of ZF+Choice) that any type can be well-ordered? Is there any theory of ordinals developed in Isabelle/HOL?)
Thank you in advance,
Andrei Popescu
Last updated: May 03 2024 at 08:18 UTC