equal
deleted
inserted
replaced
1 (* Author: Johannes Hoelzl, TU Muenchen *) |
1 (* Author: Johannes Hoelzl, TU Muenchen *) |
2 |
2 |
3 header {* A type for positive real numbers with infinity *} |
3 header {* A type for positive real numbers with infinity *} |
4 |
4 |
5 theory Positive_Extended_Real |
5 theory Positive_Extended_Real |
6 imports Complex_Main Nat_Bijection Multivariate_Analysis |
6 imports Complex_Main "~~/src/HOL/Library/Nat_Bijection" Multivariate_Analysis |
7 begin |
7 begin |
8 |
8 |
9 lemma (in complete_lattice) Sup_start: |
9 lemma (in complete_lattice) Sup_start: |
10 assumes *: "\<And>x. f x \<le> f 0" |
10 assumes *: "\<And>x. f x \<le> f 0" |
11 shows "(SUP n. f n) = f 0" |
11 shows "(SUP n. f n) = f 0" |