src/HOL/Complete_Lattices.thy
changeset 60172 423273355b55
parent 58889 5b7a9633cfa8
child 60307 75e1aa7a450e
     1.1 --- a/src/HOL/Complete_Lattices.thy	Mon May 04 16:01:36 2015 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Mon May 04 17:35:31 2015 +0200
     1.3 @@ -556,6 +556,14 @@
     1.4    shows "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
     1.5    using `mono f` by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD)
     1.6  
     1.7 +lemma mono_INF:
     1.8 +  "f (INF i : I. A i) \<le> (INF x : I. f (A x))"
     1.9 +  by (intro complete_lattice_class.INF_greatest monoD[OF `mono f`] INF_lower)
    1.10 +
    1.11 +lemma mono_SUP:
    1.12 +  "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
    1.13 +  by (intro complete_lattice_class.SUP_least monoD[OF `mono f`] SUP_upper)
    1.14 +
    1.15  end
    1.16  
    1.17  end