*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] FuncSet without extensional?*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Sat, 18 Sep 2010 20:18:30 +0200*Sender*: Joachim Breitner <msg at 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 -- 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**

**Follow-Ups**:**Re: [isabelle] FuncSet without extensional?***From:*Lawrence Paulson

**Re: [isabelle] FuncSet without extensional?***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Unicode (Was: Update on I3P)
- Next by Date: Re: [isabelle] FuncSet without extensional?
- Previous by Thread: Re: [isabelle] FOLP/simp.ML
- Next by Thread: Re: [isabelle] FuncSet without extensional?
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list