# Re: [isabelle] FuncSet without extensional?

```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

Am Samstag, den 18.09.2010, 22:16 +0200 schrieb Tobias Nipkow:
> 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:
> > 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
> >
> >
>
>

--
Joachim Breitner
e-Mail: mail at joachim-breitner.de
Homepage: http://www.joachim-breitner.de
ICQ#: 74513189
Jabber-ID: nomeata at joachim-breitner.de
```

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.