equal
deleted
inserted
replaced
933 defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}" |
933 defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}" |
934 |
934 |
935 lemma real_CauchyI: |
935 lemma real_CauchyI: |
936 assumes "Cauchy X" |
936 assumes "Cauchy X" |
937 shows "real_Cauchy X" |
937 shows "real_Cauchy X" |
938 by unfold_locales (fact assms) |
938 proof qed (fact assms) |
939 |
939 |
940 lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" |
940 lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" |
941 by (unfold S_def, auto) |
941 by (unfold S_def, auto) |
942 |
942 |
943 lemma (in real_Cauchy) bound_isUb: |
943 lemma (in real_Cauchy) bound_isUb: |