62 |
62 |
63 subsubsection{* Properties of minim *} |
63 subsubsection{* Properties of minim *} |
64 |
64 |
65 lemma minim_Under: |
65 lemma minim_Under: |
66 "\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B" |
66 "\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B" |
67 by(auto simp add: Under_def |
67 by(auto simp add: Under_def minim_inField minim_least) |
68 minim_in |
|
69 minim_inField |
|
70 minim_least |
|
71 under_ofilter |
|
72 underS_ofilter |
|
73 Field_ofilter |
|
74 ofilter_Under |
|
75 ofilter_UnderS |
|
76 ofilter_Un |
|
77 ) |
|
78 |
68 |
79 lemma equals_minim_Under: |
69 lemma equals_minim_Under: |
80 "\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk> |
70 "\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk> |
81 \<Longrightarrow> a = minim B" |
71 \<Longrightarrow> a = minim B" |
82 by(auto simp add: Under_def equals_minim) |
72 by(auto simp add: Under_def equals_minim) |
408 (* *) |
398 (* *) |
409 ultimately show ?thesis by blast |
399 ultimately show ?thesis by blast |
410 qed |
400 qed |
411 |
401 |
412 |
402 |
413 subsubsection {* Properties of order filters *} |
403 subsubsection {* Properties of order filters *} |
|
404 |
|
405 lemma ofilter_Under[simp]: |
|
406 assumes "A \<le> Field r" |
|
407 shows "ofilter(Under A)" |
|
408 proof(unfold ofilter_def, auto) |
|
409 fix x assume "x \<in> Under A" |
|
410 thus "x \<in> Field r" |
|
411 using Under_Field assms by auto |
|
412 next |
|
413 fix a x |
|
414 assume "a \<in> Under A" and "x \<in> under a" |
|
415 thus "x \<in> Under A" |
|
416 using TRANS under_Under_trans by auto |
|
417 qed |
|
418 |
|
419 lemma ofilter_UnderS[simp]: |
|
420 assumes "A \<le> Field r" |
|
421 shows "ofilter(UnderS A)" |
|
422 proof(unfold ofilter_def, auto) |
|
423 fix x assume "x \<in> UnderS A" |
|
424 thus "x \<in> Field r" |
|
425 using UnderS_Field assms by auto |
|
426 next |
|
427 fix a x |
|
428 assume "a \<in> UnderS A" and "x \<in> under a" |
|
429 thus "x \<in> UnderS A" |
|
430 using TRANS ANTISYM under_UnderS_trans by auto |
|
431 qed |
|
432 |
|
433 lemma ofilter_Int[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)" |
|
434 unfolding ofilter_def by blast |
|
435 |
|
436 lemma ofilter_Un[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A \<union> B)" |
|
437 unfolding ofilter_def by blast |
414 |
438 |
415 lemma ofilter_INTER: |
439 lemma ofilter_INTER: |
416 "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)" |
440 "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)" |
417 unfolding ofilter_def by blast |
441 unfolding ofilter_def by blast |
418 |
442 |