environ
vocabularies HIDDEN, MATROID0, NAT_1, FINSET_1, CARD_1, ARYTM_3, SUBSET_1, XXREAL_0, CLASSES1, SGRAPH1, SIMPLEX0, TARSKI, GRAPH_1, GLIB_000, PBOOLE, XBOOLE_0, ZFMISC_1, NUMBERS, FUNCT_1, RELAT_1, COMBGRAS, MYCIELSK, DILWORTH, CIRCUIT2, AOFA_000, EQREL_1, PEPIN, CIRCUIT1, FUNCT_2, ARYTM_1, PROB_1, BSPACE, STRUCT_0, NEWTON, STIRL2_1, UPROOTS, FINSEQ_1, CARD_3, FINSEQ_2, PROB_2, GROUP_10, RAMSEY_1, SCMYCIEL;
notations HIDDEN, TARSKI, XBOOLE_0, ORDINAL1, RELAT_1, FUNCT_1, FUNCT_2, MATROID0, XCMPLX_0, NAT_1, FINSET_1, ENUMSET1, FINSEQ_1, FINSEQ_2, CARD_1, SUBSET_1, XXREAL_0, ZFMISC_1, NUMBERS, NEWTON, UPROOTS, RVSUM_1, PROB_2, FUNCOP_1, CLASSES1, AOFA_000, EQREL_1, BSPACE, STIRL2_1, PBOOLE, CARD_LAR, MYCIELSK, GROUP_10, RAMSEY_1, CARD_3;
definitions TARSKI, XBOOLE_0, FUNCT_1, CLASSES1, FINSET_1;
theorems TARSKI, XXREAL_0, XBOOLE_0, NAT_1, ZFMISC_1, ENUMSET1, CARD_1, CARD_2, EULER_1, FUNCT_1, FUNCT_2, EQREL_1, FINSET_1, XREAL_1, MYCIELSK, XBOOLE_1, BSPACE, CLASSES1, XREGULAR, WELLORD2, STIRL2_1, RVSUM_1, DIST_1, FINSEQ_3, FINSEQ_1, FUNCOP_1, PROB_2, FINSEQ_2, DILWORTH, PENCIL_1, RELAT_1, PARTFUN1, PBOOLE, NEWTON, RAMSEY_1, TOPGEN_2, SUBSET_1, ORDERS_1, FINSEQ_4, XTUPLE_0;
schemes CLASSES1, FUNCT_1, FUNCT_2, NAT_1, FRAENKEL, SUBSET_1, RECDEF_1, PRE_CIRC, FINSEQ_2;
registrations FINSET_1, XXREAL_0, ORDINAL1, SETFAM_1, RELSET_1, XREAL_0, NAT_1, SUBSET_1, EQREL_1, CARD_1, NEWTON, VALUED_0, XBOOLE_0, PARTFUN1, FUNCT_2, SIMPLEX0, MYCIELSK, ZFMISC_1, FINSEQ_1, COHSP_1, STIRL2_1;
constructors HIDDEN, MATROID0, LEXBFS, UPROOTS, CARD_LAR, RVSUM_1, BSPACE, STIRL2_1, BINOP_2, PROB_2, DOMAIN_1, CLASSES1, MYCIELSK, RAMSEY_1, RELSET_1, COHSP_1;
requirements HIDDEN, SUBSET, NUMERALS, REAL, ARITHM, BOOLE;
equalities TARSKI, MYCIELSK, BSPACE, FINSEQ_2, GROUP_10, EQREL_1, CARD_3, CARD_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, FUNCT_1, FINSET_1;
defpred S1[ set ] means verum;
theorem Th4:
for
x1,
y1,
x2,
y2 being
object for
X being
set st
x1 in X &
x2 in X &
{x1,[y1,X]} = {x2,[y2,X]} holds
(
x1 = x2 &
y1 = y2 )
Lm1:
for X being set holds union { V where V is finite Subset of X : card V <= 2 } = X
Lm2:
for n being Nat holds {{}} is n -at_most_dimensional
Lm3:
for G being SimpleGraph holds (CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph
Lm4:
for G being SimpleGraph holds Vertices G = Vertices ((CompleteSGraph (Vertices G)) \ (Edges G))
Lm5:
for G being SimpleGraph
for x, y being set st x <> y & x in Vertices G & y in Vertices G holds
( {x,y} in Edges G iff {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) )
Lm6:
for G, CG being SimpleGraph st CG = (CompleteSGraph (Vertices G)) \ (Edges G) holds
(CompleteSGraph (Vertices CG)) \ (Edges CG) = G
Lm7:
for G being SimpleGraph
for L, x being set st x in Vertices (G SubgraphInducedBy L) holds
x in L
Lm8:
for G being SimpleGraph
for L, x being set st x in L & x in Vertices G holds
x in Vertices (G SubgraphInducedBy L)
Lm9:
for G being SimpleGraph
for L being set st L c= Vertices G holds
Vertices (G SubgraphInducedBy L) = L
Lm10:
for G being SimpleGraph
for L, x, y being set st x in L & y in L & {x,y} in G holds
{x,y} in G SubgraphInducedBy L