equal
deleted
inserted
replaced
46 eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def |
46 eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def |
47 simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+ |
47 simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+ |
48 |
48 |
49 lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)" |
49 lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)" |
50 and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)" |
50 and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)" |
51 by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib setsum_delta |
51 by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib comm_monoid_add_class.setsum.delta |
52 cong: if_cong) |
52 cong: if_cong) |
53 |
53 |
54 lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)" |
54 lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)" |
55 and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)" |
55 and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)" |
56 using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def) |
56 using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def) |
117 and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b" |
117 and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b" |
118 by auto |
118 by auto |
119 hence "Inf ?proj = x \<bullet> b" |
119 hence "Inf ?proj = x \<bullet> b" |
120 by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq) |
120 by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq) |
121 hence "x \<bullet> b = Inf X \<bullet> b" |
121 hence "x \<bullet> b = Inf X \<bullet> b" |
122 by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta |
122 by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum.delta |
123 simp del: Inf_class.Inf_image_eq |
123 simp del: Inf_class.Inf_image_eq |
124 cong: if_cong) |
124 cong: if_cong) |
125 with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast |
125 with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast |
126 qed |
126 qed |
127 |
127 |
140 and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b" |
140 and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b" |
141 by auto |
141 by auto |
142 hence "Sup ?proj = x \<bullet> b" |
142 hence "Sup ?proj = x \<bullet> b" |
143 by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq) |
143 by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq) |
144 hence "x \<bullet> b = Sup X \<bullet> b" |
144 hence "x \<bullet> b = Sup X \<bullet> b" |
145 by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta |
145 by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum.delta |
146 simp del: Sup_image_eq cong: if_cong) |
146 simp del: Sup_image_eq cong: if_cong) |
147 with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast |
147 with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast |
148 qed |
148 qed |
149 |
149 |
150 lemma (in order) atLeastatMost_empty'[simp]: |
150 lemma (in order) atLeastatMost_empty'[simp]: |