author paulson Sun Feb 25 12:54:55 2018 +0000 (15 months ago) changeset 67719 bffb7482faaa parent 67717 5a1b299fe4af child 67720 b342f96e47b5
new material on matrices, etc., and consolidating duplicate results about of_nat
```     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Sat Feb 24 17:21:35 2018 +0100
1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Sun Feb 25 12:54:55 2018 +0000
1.3 @@ -17,8 +17,11 @@
1.4  definition unit_ball_vol :: "real \<Rightarrow> real" where
1.5    "unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)"
1.6
1.7 +lemma unit_ball_vol_pos [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n > 0"
1.8 +  by (force simp: unit_ball_vol_def intro: divide_nonneg_pos)
1.9 +
1.10  lemma unit_ball_vol_nonneg [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n \<ge> 0"
1.11 -  by (auto simp add: unit_ball_vol_def intro!: divide_nonneg_pos Gamma_real_pos)
1.12 +  by (simp add: dual_order.strict_implies_order)
1.13
1.14  text \<open>
1.15    We first need the value of the following integral, which is at the core of
```
```     2.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sat Feb 24 17:21:35 2018 +0100
2.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Feb 25 12:54:55 2018 +0000
2.3 @@ -7,19 +7,6 @@
2.4  lemma subspace_special_hyperplane: "subspace {x. x \$ k = 0}"
2.6
2.7 -lemma delta_mult_idempotent:
2.8 -  "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)"
2.9 -  by simp
2.10 -
2.11 -(*move up?*)
2.12 -lemma sum_UNIV_sum:
2.13 -  fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
2.14 -  shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))"
2.15 -  apply (subst UNIV_Plus_UNIV [symmetric])
2.16 -  apply (subst sum.Plus)
2.17 -  apply simp_all
2.18 -  done
2.19 -
2.20  lemma sum_mult_product:
2.21    "sum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
2.22    unfolding sum_nat_group[of h B A, unfolded atLeast0LessThan, symmetric]
2.23 @@ -632,7 +619,7 @@
2.24      by simp
2.25  qed
2.26
2.27 -text\<open>Inverse matrices  (not necessarily square)\<close>
2.28 +subsection\<open>Inverse matrices  (not necessarily square)\<close>
2.29
2.30  definition
2.31    "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
2.32 @@ -728,9 +715,86 @@
2.33    done
2.34
2.35
2.36 -subsection \<open>lambda skolemization on cartesian products\<close>
2.37 +subsection\<open>Some bounds on components etc. relative to operator norm.\<close>
2.38 +
2.39 +lemma norm_column_le_onorm:
2.40 +  fixes A :: "real^'n^'m"
2.41 +  shows "norm(column i A) \<le> onorm(( *v) A)"
2.42 +proof -
2.43 +  have bl: "bounded_linear (( *v) A)"
2.44 +    by (simp add: linear_linear matrix_vector_mul_linear)
2.45 +  have "norm (\<chi> j. A \$ j \$ i) \<le> norm (A *v axis i 1)"
2.46 +    by (simp add: matrix_mult_dot cart_eq_inner_axis)
2.47 +  also have "\<dots> \<le> onorm (( *v) A)"
2.48 +    using onorm [OF bl, of "axis i 1"] by (auto simp: axis_in_Basis)
2.49 +  finally have "norm (\<chi> j. A \$ j \$ i) \<le> onorm (( *v) A)" .
2.50 +  then show ?thesis
2.51 +    unfolding column_def .
2.52 +qed
2.53 +
2.54 +lemma matrix_component_le_onorm:
2.55 +  fixes A :: "real^'n^'m"
2.56 +  shows "\<bar>A \$ i \$ j\<bar> \<le> onorm(( *v) A)"
2.57 +proof -
2.58 +  have "\<bar>A \$ i \$ j\<bar> \<le> norm (\<chi> n. (A \$ n \$ j))"
2.59 +    by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta)
2.60 +  also have "\<dots> \<le> onorm (( *v) A)"
2.61 +    by (metis (no_types) column_def norm_column_le_onorm)
2.62 +  finally show ?thesis .
2.63 +qed
2.64 +
2.65 +lemma component_le_onorm:
2.66 +  fixes f :: "real^'m \<Rightarrow> real^'n"
2.67 +  shows "linear f \<Longrightarrow> \<bar>matrix f \$ i \$ j\<bar> \<le> onorm f"
2.68 +  by (metis matrix_component_le_onorm matrix_vector_mul)
2.69
2.70 -(* FIXME: rename do choice_cart *)
2.71 +lemma onorm_le_matrix_component_sum:
2.72 +  fixes A :: "real^'n^'m"
2.73 +  shows "onorm(( *v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A \$ i \$ j\<bar>)"
2.74 +proof (rule onorm_le)
2.75 +  fix x
2.76 +  have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) \$ i\<bar>)"
2.77 +    by (rule norm_le_l1_cart)
2.78 +  also have "\<dots> \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A \$ i \$ j\<bar> * norm x)"
2.79 +  proof (rule sum_mono)
2.80 +    fix i
2.81 +    have "\<bar>(A *v x) \$ i\<bar> \<le> \<bar>\<Sum>j\<in>UNIV. A \$ i \$ j * x \$ j\<bar>"
2.82 +      by (simp add: matrix_vector_mult_def)
2.83 +    also have "\<dots> \<le> (\<Sum>j\<in>UNIV. \<bar>A \$ i \$ j * x \$ j\<bar>)"
2.84 +      by (rule sum_abs)
2.85 +    also have "\<dots> \<le> (\<Sum>j\<in>UNIV. \<bar>A \$ i \$ j\<bar> * norm x)"
2.86 +      by (rule sum_mono) (simp add: abs_mult component_le_norm_cart mult_left_mono)
2.87 +    finally show "\<bar>(A *v x) \$ i\<bar> \<le> (\<Sum>j\<in>UNIV. \<bar>A \$ i \$ j\<bar> * norm x)" .
2.88 +  qed
2.89 +  finally show "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A \$ i \$ j\<bar>) * norm x"
2.90 +    by (simp add: sum_distrib_right)
2.91 +qed
2.92 +
2.93 +lemma onorm_le_matrix_component:
2.94 +  fixes A :: "real^'n^'m"
2.95 +  assumes "\<And>i j. abs(A\$i\$j) \<le> B"
2.96 +  shows "onorm(( *v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
2.97 +proof (rule onorm_le)
2.98 +  fix x :: "(real, 'n) vec"
2.99 +  have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) \$ i\<bar>)"
2.100 +    by (rule norm_le_l1_cart)
2.101 +  also have "\<dots> \<le> (\<Sum>i::'m \<in>UNIV. real (CARD('n)) * B * norm x)"
2.102 +  proof (rule sum_mono)
2.103 +    fix i
2.104 +    have "\<bar>(A *v x) \$ i\<bar> \<le> norm(A \$ i) * norm x"
2.105 +      by (simp add: matrix_mult_dot Cauchy_Schwarz_ineq2)
2.106 +    also have "\<dots> \<le> (\<Sum>j\<in>UNIV. \<bar>A \$ i \$ j\<bar>) * norm x"
2.107 +      by (simp add: mult_right_mono norm_le_l1_cart)
2.108 +    also have "\<dots> \<le> real (CARD('n)) * B * norm x"
2.109 +      by (simp add: assms sum_bounded_above mult_right_mono)
2.110 +    finally show "\<bar>(A *v x) \$ i\<bar> \<le> real (CARD('n)) * B * norm x" .
2.111 +  qed
2.112 +  also have "\<dots> \<le> CARD('m) * real (CARD('n)) * B * norm x"
2.113 +    by simp
2.114 +  finally show "norm (A *v x) \<le> CARD('m) * real (CARD('n)) * B * norm x" .
2.115 +qed
2.116 +
2.117 +subsection \<open>lambda skolemization on cartesian products\<close>
2.118
2.119  lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
2.120     (\<exists>x::'a ^ 'n. \<forall>i. P i (x \$ i))" (is "?lhs \<longleftrightarrow> ?rhs")
2.121 @@ -751,6 +815,32 @@
2.122    ultimately show ?thesis by metis
2.123  qed
2.124
2.125 +lemma rational_approximation:
2.126 +  assumes "e > 0"
2.127 +  obtains r::real where "r \<in> \<rat>" "\<bar>r - x\<bar> < e"
2.128 +  using Rats_dense_in_real [of "x - e/2" "x + e/2"] assms by auto
2.129 +
2.130 +lemma matrix_rational_approximation:
2.131 +  fixes A :: "real^'n^'m"
2.132 +  assumes "e > 0"
2.133 +  obtains B where "\<And>i j. B\$i\$j \<in> \<rat>" "onorm(\<lambda>x. (A - B) *v x) < e"
2.134 +proof -
2.135 +  have "\<forall>i j. \<exists>q \<in> \<rat>. \<bar>q - A \$ i \$ j\<bar> < e / (2 * CARD('m) * CARD('n))"
2.136 +    using assms by (force intro: rational_approximation [of "e / (2 * CARD('m) * CARD('n))"])
2.137 +  then obtain B where B: "\<And>i j. B\$i\$j \<in> \<rat>" and Bclo: "\<And>i j. \<bar>B\$i\$j - A \$ i \$ j\<bar> < e / (2 * CARD('m) * CARD('n))"
2.138 +    by (auto simp: lambda_skolem Bex_def)
2.139 +  show ?thesis
2.140 +  proof
2.141 +    have "onorm (( *v) (A - B)) \<le> real CARD('m) * real CARD('n) *
2.142 +    (e / (2 * real CARD('m) * real CARD('n)))"
2.143 +      apply (rule onorm_le_matrix_component)
2.144 +      using Bclo by (simp add: abs_minus_commute less_imp_le)
2.145 +    also have "\<dots> < e"
2.146 +      using \<open>0 < e\<close> by (simp add: divide_simps)
2.147 +    finally show "onorm (( *v) (A - B)) < e" .
2.148 +  qed (use B in auto)
2.149 +qed
2.150 +
2.151  lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
2.152    unfolding inner_simps scalar_mult_eq_scaleR by auto
2.153
2.154 @@ -1139,7 +1229,7 @@
2.155      and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i. (b\$i \<le> a\$i \<or> d\$i \<le> c\$i \<or> b\$i \<le> c\$i \<or> d\$i \<le> a\$i))" (is ?th4)
2.156    using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis)
2.157
2.158 -lemma inter_interval_cart:
2.159 +lemma Int_interval_cart:
2.160    fixes a :: "real^'n"
2.161    shows "cbox a b \<inter> cbox c d =  {(\<chi> i. max (a\$i) (c\$i)) .. (\<chi> i. min (b\$i) (d\$i))}"
2.162    unfolding Int_interval
2.163 @@ -1225,6 +1315,11 @@
2.164      by (auto simp: axis_eq_axis inj_on_def *)
2.165  qed
2.166
2.167 +lemma dim_subset_UNIV_cart:
2.168 +  fixes S :: "(real^'n) set"
2.169 +  shows "dim S \<le> CARD('n)"
2.170 +  by (metis dim_subset_UNIV DIM_cart DIM_real mult.right_neutral)
2.171 +
2.172  lemma affinity_inverses:
2.173    assumes m0: "m \<noteq> (0::'a::field)"
2.174    shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
2.175 @@ -1430,13 +1525,7 @@
2.176    unfolding vector_def by simp_all
2.177
2.178  lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
2.179 -  apply auto
2.180 -  apply (erule_tac x="v\$1" in allE)
2.181 -  apply (subgoal_tac "vector [v\$1] = v")
2.182 -  apply simp
2.183 -  apply (vector vector_def)
2.184 -  apply simp
2.185 -  done
2.186 +  by (metis vector_1 vector_one)
2.187
2.188  lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
2.189    apply auto
```
```     3.1 --- a/src/HOL/Analysis/Great_Picard.thy	Sat Feb 24 17:21:35 2018 +0100
3.2 +++ b/src/HOL/Analysis/Great_Picard.thy	Sun Feb 25 12:54:55 2018 +0000
3.3 @@ -46,7 +46,7 @@
3.4    have "(n-1)^2 \<le> n^2 - 1"
3.5      using assms by (simp add: algebra_simps power2_eq_square)
3.6    then have "real (n - 1) \<le> sqrt (real (n\<^sup>2 - 1))"
3.7 -    by (metis Extended_Nonnegative_Real.of_nat_le_iff of_nat_power real_le_rsqrt)
3.8 +    by (metis of_nat_le_iff of_nat_power real_le_rsqrt)
3.9    then have "n-1 \<le> sqrt(real n ^ 2 - 1)"
3.10      by (simp add: Suc_leI assms of_nat_diff)
3.11    then show ?thesis
```
```     4.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Feb 24 17:21:35 2018 +0100
4.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Feb 25 12:54:55 2018 +0000
4.3 @@ -46,6 +46,14 @@
4.4  lemma content_cbox_if: "content (cbox a b) = (if cbox a b = {} then 0 else \<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
4.6
4.7 +lemma content_cbox_cart:
4.8 +   "cbox a b \<noteq> {} \<Longrightarrow> content(cbox a b) = prod (\<lambda>i. b\$i - a\$i) UNIV"
4.9 +  by (simp add: content_cbox_if Basis_vec_def cart_eq_inner_axis axis_eq_axis prod.UNION_disjoint)
4.10 +
4.11 +lemma content_cbox_if_cart:
4.12 +   "content(cbox a b) = (if cbox a b = {} then 0 else prod (\<lambda>i. b\$i - a\$i) UNIV)"
4.13 +  by (simp add: content_cbox_cart)
4.14 +
4.15  lemma content_division_of:
4.16    assumes "K \<in> \<D>" "\<D> division_of S"
4.17    shows "content K = (\<Prod>i \<in> Basis. interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)"
4.18 @@ -357,6 +365,9 @@
4.19    unfolding integral_def
4.20    by (rule some_equality) (auto intro: has_integral_unique)
4.21
4.22 +lemma has_integral_iff: "(f has_integral i) S \<longleftrightarrow> (f integrable_on S \<and> integral S f = i)"
4.23 +  by blast
4.24 +
4.25  lemma eq_integralD: "integral k f = y \<Longrightarrow> (f has_integral y) k \<or> ~ f integrable_on k \<and> y=0"
4.26    unfolding integral_def integrable_on_def
4.27    apply (erule subst)
4.28 @@ -3005,7 +3016,6 @@
4.29    shows "f integrable_on {c..d}"
4.30    by (metis assms box_real(2) integrable_subinterval)
4.31
4.32 -
4.33  subsection \<open>Combining adjacent intervals in 1 dimension.\<close>
4.34
4.35  lemma has_integral_combine:
4.36 @@ -4673,6 +4683,46 @@
4.37      using as by auto
4.38  qed
4.39
4.40 +subsection\<open>Integrals on set differences\<close>
4.41 +
4.42 +lemma has_integral_setdiff:
4.43 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
4.44 +  assumes S: "(f has_integral i) S" and T: "(f has_integral j) T"
4.45 +    and neg: "negligible (T - S)"
4.46 +  shows "(f has_integral (i - j)) (S - T)"
4.47 +proof -
4.48 +  show ?thesis
4.49 +    unfolding has_integral_restrict_UNIV [symmetric, of f]
4.50 +  proof (rule has_integral_spike [OF neg])
4.51 +    have eq: "(\<lambda>x. (if x \<in> S then f x else 0) - (if x \<in> T then f x else 0)) =
4.52 +            (\<lambda>x. if x \<in> T - S then - f x else if x \<in> S - T then f x else 0)"
4.53 +      by (force simp add: )
4.54 +    have "((\<lambda>x. if x \<in> S then f x else 0) has_integral i) UNIV"
4.55 +      "((\<lambda>x. if x \<in> T then f x else 0) has_integral j) UNIV"
4.56 +      using S T has_integral_restrict_UNIV by auto
4.57 +    from has_integral_diff [OF this]
4.58 +    show "((\<lambda>x. if x \<in> T - S then - f x else if x \<in> S - T then f x else 0)
4.59 +                   has_integral i-j) UNIV"
4.60 +      by (simp add: eq)
4.61 +  qed force
4.62 +qed
4.63 +
4.64 +lemma integral_setdiff:
4.65 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
4.66 +  assumes "f integrable_on S" "f integrable_on T" "negligible(T - S)"
4.67 + shows "integral (S - T) f = integral S f - integral T f"
4.68 +  by (rule integral_unique) (simp add: assms has_integral_setdiff integrable_integral)
4.69 +
4.70 +lemma integrable_setdiff:
4.71 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
4.72 +  assumes "(f has_integral i) S" "(f has_integral j) T" "negligible (T - S)"
4.73 +  shows "f integrable_on (S - T)"
4.74 +  using has_integral_setdiff [OF assms]
4.75 +  by (simp add: has_integral_iff)
4.76 +
4.77 +lemma negligible_setdiff [simp]: "T \<subseteq> S \<Longrightarrow> negligible (T - S)"
4.78 +  by (metis Diff_eq_empty_iff negligible_empty)
4.79 +
4.80  lemma negligible_on_intervals: "negligible s \<longleftrightarrow> (\<forall>a b. negligible(s \<inter> cbox a b))" (is "?l \<longleftrightarrow> ?r")
4.81  proof
4.82    assume ?r
4.83 @@ -4757,9 +4807,7 @@
4.84  lemma has_integral_closure:
4.85    fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
4.86    shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (closure S) \<longleftrightarrow> (f has_integral y) S"
4.87 -  apply (rule has_integral_spike_set_eq)
4.88 -  apply (auto simp: Un_Diff closure_Un_frontier negligible_diff)
4.89 -  by (simp add: Diff_eq closure_Un_frontier)
4.90 +  by (rule has_integral_spike_set_eq) (simp add: Un_Diff closure_Un_frontier negligible_diff)
4.91
4.92  lemma has_integral_open_interval:
4.93    fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
4.94 @@ -5344,9 +5392,6 @@
4.95
4.96  subsection \<open>Also tagged divisions\<close>
4.97
4.98 -lemma has_integral_iff: "(f has_integral i) S \<longleftrightarrow> (f integrable_on S \<and> integral S f = i)"
4.99 -  by blast
4.100 -
4.101  lemma has_integral_combine_tagged_division:
4.102    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
4.103    assumes "p tagged_division_of S"
```
```     5.1 --- a/src/HOL/HOL.thy	Sat Feb 24 17:21:35 2018 +0100
5.2 +++ b/src/HOL/HOL.thy	Sun Feb 25 12:54:55 2018 +0000
5.3 @@ -1404,6 +1404,9 @@
5.4  lemma ex_if_distrib: "(\<exists>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<or> (\<exists>x. x\<noteq>a \<and> Q x)"
5.5    by auto
5.6
5.7 +lemma if_if_eq_conj: "(if P then if Q then x else y else y) = (if P \<and> Q then x else y)"
5.8 +  by simp
5.9 +
5.10  text \<open>As a simplification rule, it replaces all function equalities by
5.11    first-order equalities.\<close>
5.12  lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
```
```     6.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sat Feb 24 17:21:35 2018 +0100
6.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Feb 25 12:54:55 2018 +0000
6.3 @@ -158,17 +158,6 @@
6.4    using tendsto_cmult_ereal[of c f "f x" "at x within A" for x]
6.5    by (auto simp: continuous_on_def simp del: tendsto_cmult_ereal)
6.6
6.7 -context linordered_nonzero_semiring
6.8 -begin
6.9 -
6.10 -lemma of_nat_nonneg [simp]: "0 \<le> of_nat n"
6.11 -  by (induct n) simp_all
6.12 -
6.13 -lemma of_nat_mono[simp]: "i \<le> j \<Longrightarrow> of_nat i \<le> of_nat j"
6.15 -
6.16 -end
6.17 -
6.18  lemma real_of_nat_Sup:
6.19    assumes "A \<noteq> {}" "bdd_above A"
6.20    shows "of_nat (Sup A) = (SUP a:A. of_nat a :: real)"
6.21 @@ -181,21 +170,6 @@
6.22      by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
6.23  qed
6.24
6.25 -\<comment> \<open>These generalise their counterparts in \<open>Nat.linordered_semidom_class\<close>\<close>
6.26 -lemma of_nat_less[simp]:
6.27 -  "m < n \<Longrightarrow> of_nat m < (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0})"
6.28 -  by (auto simp: less_le)
6.29 -
6.30 -lemma of_nat_le_iff[simp]:
6.31 -  "of_nat m \<le> (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0}) \<longleftrightarrow> m \<le> n"
6.32 -proof (safe intro!: of_nat_mono)
6.33 -  assume "of_nat m \<le> (of_nat n::'a)" then show "m \<le> n"
6.34 -  proof (intro leI notI)
6.35 -    assume "n < m" from less_le_trans[OF of_nat_less[OF this] \<open>of_nat m \<le> of_nat n\<close>] show False
6.36 -      by blast
6.37 -  qed
6.38 -qed
6.39 -
6.40  lemma (in complete_lattice) SUP_sup_const1:
6.41    "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup c (f i)) = sup c (SUP i:I. f i)"
6.42    using SUP_sup_distrib[of "\<lambda>_. c" I f] by simp
```