# Re: [isabelle] FuncSet without extensional?

Extensionality isn't always wanted, so the concepts are defined separately. Possibly you want a new definition of hom.
Larry Paulson
On 18 Sep 2010, at 19:18, Joachim Breitner wrote:
> 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

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