equal
deleted
inserted
replaced
357 |
357 |
358 syntax (xsymbols) |
358 syntax (xsymbols) |
359 "MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10) |
359 "MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10) |
360 "INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10) |
360 "INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10) |
361 |
361 |
|
362 syntax (HTML output) |
|
363 "MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10) |
|
364 "INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10) |
|
365 |
362 lemma INF_EX: |
366 lemma INF_EX: |
363 "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" |
367 "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" |
364 proof (unfold INF_def, rule ccontr) |
368 proof (unfold INF_def, rule ccontr) |
365 assume inf: "infinite {x. P x}" |
369 assume inf: "infinite {x. P x}" |
366 and notP: "\<not>(\<exists>x. P x)" |
370 and notP: "\<not>(\<exists>x. P x)" |