[isabelle] FuncSet without extensional?



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.