equal
deleted
inserted
replaced
29 definition |
29 definition |
30 Symmetric :: "i=>o" where |
30 Symmetric :: "i=>o" where |
31 "Symmetric(E) == (\<forall>x y. <x,y>:E \<longrightarrow> <y,x>:E)" |
31 "Symmetric(E) == (\<forall>x y. <x,y>:E \<longrightarrow> <y,x>:E)" |
32 |
32 |
33 definition |
33 definition |
34 Atleast :: "[i,i]=>o" where \<comment> "not really necessary: ZF defines cardinality" |
34 Atleast :: "[i,i]=>o" where \<comment> \<open>not really necessary: ZF defines cardinality\<close> |
35 "Atleast(n,S) == (\<exists>f. f \<in> inj(n,S))" |
35 "Atleast(n,S) == (\<exists>f. f \<in> inj(n,S))" |
36 |
36 |
37 definition |
37 definition |
38 Clique :: "[i,i,i]=>o" where |
38 Clique :: "[i,i,i]=>o" where |
39 "Clique(C,V,E) == (C \<subseteq> V) & (\<forall>x \<in> C. \<forall>y \<in> C. x\<noteq>y \<longrightarrow> <x,y> \<in> E)" |
39 "Clique(C,V,E) == (C \<subseteq> V) & (\<forall>x \<in> C. \<forall>y \<in> C. x\<noteq>y \<longrightarrow> <x,y> \<in> E)" |