equal
deleted
inserted
replaced
1113 |
1113 |
1114 end |
1114 end |
1115 |
1115 |
1116 |
1116 |
1117 subsubsection \<open>Properties in more restricted classes of structures\<close> |
1117 subsubsection \<open>Properties in more restricted classes of structures\<close> |
|
1118 |
|
1119 context linordered_nonzero_semiring |
|
1120 begin |
|
1121 |
|
1122 lemma prod_ge_1: "(\<And>x. x \<in> A \<Longrightarrow> 1 \<le> f x) \<Longrightarrow> 1 \<le> prod f A" |
|
1123 proof (induct A rule: infinite_finite_induct) |
|
1124 case infinite |
|
1125 then show ?case by simp |
|
1126 next |
|
1127 case empty |
|
1128 then show ?case by simp |
|
1129 next |
|
1130 case (insert x F) |
|
1131 have "1 * 1 \<le> f x * prod f F" |
|
1132 by (rule mult_mono') (use insert in auto) |
|
1133 with insert show ?case by simp |
|
1134 qed |
|
1135 |
|
1136 lemma prod_le_1: |
|
1137 fixes f :: "'b \<Rightarrow> 'a" |
|
1138 assumes "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x \<and> f x \<le> 1" |
|
1139 shows "prod f A \<le> 1" |
|
1140 using assms |
|
1141 proof (induct A rule: infinite_finite_induct) |
|
1142 case infinite |
|
1143 then show ?case by simp |
|
1144 next |
|
1145 case empty |
|
1146 then show ?case by simp |
|
1147 next |
|
1148 case (insert x F) |
|
1149 then show ?case by (force simp: mult.commute intro: dest: mult_le_one) |
|
1150 qed |
|
1151 |
|
1152 end |
1118 |
1153 |
1119 context comm_semiring_1 |
1154 context comm_semiring_1 |
1120 begin |
1155 begin |
1121 |
1156 |
1122 lemma dvd_prod_eqI [intro]: |
1157 lemma dvd_prod_eqI [intro]: |