equal
deleted
inserted
replaced
7 theory Integration |
7 theory Integration |
8 imports |
8 imports |
9 Derivative |
9 Derivative |
10 Uniform_Limit |
10 Uniform_Limit |
11 "~~/src/HOL/Library/Indicator_Function" |
11 "~~/src/HOL/Library/Indicator_Function" |
12 Bounded_Linear_Function |
|
13 begin |
12 begin |
14 |
13 |
15 lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *) |
14 lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *) |
16 fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" |
15 fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" |
17 shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a" |
16 shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a" |