# Re: [isabelle] FuncSet without extensional?

Since this is a library theory, you can expect a number of client
theories to break if you make such a drastic change. For example
lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
within FuncSet would no longer hold, although it is a standard law about
function spaces.
At the moment users have the choice: they can always adjoin
"extensional" in their context if needed. Your suggestion deprives them
of that choice.
Tobias
Joachim Breitner schrieb:
> 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
>
>

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