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.