[isabelle] FuncSet without extensional?


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

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:

  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"?


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.