Email Gateway (Aug 18 2022 at 16:08): Email Gateway (Aug 18 2022 at 16:08):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
I was trying to prove the statement that there is a bijection between
Hom(F(X),C2) and Pow(X). I started with
"∃ f. bij_betw f (Pow X) (hom (ℱ\<^bsub>X\<^esub>) C2)"
and it went relatively well... until I noticed that hom is not suitable
here. Group.hom is defined via FuncSet.Pi, which has the following
definition:
Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where
"Pi A B = {f. ∀x. x ∈ A --> f x ∈ B x}"
(With an abbreviation A -> B).
This means that for example ({} -> {}) is not a one-element-set, but is
actually the set UNIV::('a -> 'b).
Right below the definition of Pi, there is a predicate specifying that
functions are undefined outside their definition:
definition
extensional :: "'a set => ('a => 'b) set" where
"extensional A = {f. ∀x. x~:A --> f x = undefined}"
For my current goal, it would be great if this were part of the
definition of Pi. Would this be generally useful? Or are there hard
reasons not to require "extensional A" for function in "A -> B"?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:08):From: Lawrence Paulson <lp15@cam.ac.uk>
Extensionality isn't always wanted, so the concepts are defined separately. Possibly you want a new definition of hom.
Larry Paulson
Email Gateway (Aug 18 2022 at 16:08):From: Tobias Nipkow <nipkow@in.tum.de>
Since this is a library theory, you can expect a number of client
theories to break if you make such a drastic change. For example
lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
within FuncSet would no longer hold, although it is a standard law about
function spaces.
At the moment users have the choice: they can always adjoin
"extensional" in their context if needed. Your suggestion deprives them
of that choice.
Tobias
Joachim Breitner schrieb:
Email Gateway (Aug 18 2022 at 16:08):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
points taken. I’ll try with a definition homr here, combining hom and
extensional.
But assuming one would give hom or iso more structure (e.g. a group
structure), then demanding extensionality would be required, e.g. for
the uniqueness of \<one>.
BTW, are there already theories about uncountable sets? I’d need, as a
lemma, the fact that the M* (the set of finite words) of a uncountably
infinte set M has the same cardinality.
Thanks,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC