equal
deleted
inserted
replaced
107 |
107 |
108 lemma merge_vimage: |
108 lemma merge_vimage: |
109 "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^sub>E (I \<union> J) E = Pi I E \<times> Pi J E" |
109 "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^sub>E (I \<union> J) E = Pi I E \<times> Pi J E" |
110 by (auto simp: restrict_Pi_cancel PiE_def) |
110 by (auto simp: restrict_Pi_cancel PiE_def) |
111 |
111 |
112 subsection%important \<open>Finite product spaces\<close> |
112 subsection \<open>Finite product spaces\<close> |
113 |
113 |
114 subsubsection%important \<open>Products\<close> |
114 subsubsection \<open>Products\<close> |
115 |
115 |
116 definition%important prod_emb where |
116 definition%important prod_emb where |
117 "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
117 "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
118 |
118 |
119 lemma prod_emb_iff: |
119 lemma prod_emb_iff: |