equal
deleted
inserted
replaced
968 show "\<exists>a b::real. a \<noteq> b" |
968 show "\<exists>a b::real. a \<noteq> b" |
969 using zero_neq_one by blast |
969 using zero_neq_one by blast |
970 qed |
970 qed |
971 end |
971 end |
972 |
972 |
973 text {* |
|
974 \medskip Completeness properties using @{text "isUb"}, @{text "isLub"}: |
|
975 *} |
|
976 |
|
977 lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t" |
|
978 by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper) |
|
979 |
|
980 |
973 |
981 subsection {* Hiding implementation details *} |
974 subsection {* Hiding implementation details *} |
982 |
975 |
983 hide_const (open) vanishes cauchy positive Real |
976 hide_const (open) vanishes cauchy positive Real |
984 |
977 |