equal
deleted
inserted
replaced
5 section \<open>Pi and Function Sets\<close> |
5 section \<open>Pi and Function Sets\<close> |
6 |
6 |
7 theory FuncSet |
7 theory FuncSet |
8 imports Main |
8 imports Main |
9 abbrevs PiE = "Pi\<^sub>E" |
9 abbrevs PiE = "Pi\<^sub>E" |
10 PIE = "\<Pi>\<^sub>E" |
10 and PIE = "\<Pi>\<^sub>E" |
11 begin |
11 begin |
12 |
12 |
13 definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
13 definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
14 where "Pi A B = {f. \<forall>x. x \<in> A \<longrightarrow> f x \<in> B x}" |
14 where "Pi A B = {f. \<forall>x. x \<in> A \<longrightarrow> f x \<in> B x}" |
15 |
15 |