diff --git a/content/http..mathhub.info/MitM/Foundation/$Description$Operator.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/$Description$Operator.omdoc.xz index aec127769356965cd64f85cea11fb622b50df623..acfccf012962e80393c830cfefe7ad48ab1e7883 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/$Description$Operator.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/$Description$Operator.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/$Informal$Proofs.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/$Informal$Proofs.omdoc.xz index 0007e5a1d2430cd9d1f62b75a183a095d45cde06..146e9046eb8d7376dba4774235a0e54b4a0adc28 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/$Informal$Proofs.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/$Informal$Proofs.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/$Logic.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/$Logic.omdoc.xz index 139b3dcfbc0aecd2c85f610bf8b9fb4e5aa90a21..9ae61cfc04c41da0f0d56e693169dc6a36fc5b2f 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/$Logic.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/$Logic.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/$Matrices.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/$Matrices.omdoc.xz index 7edae7133a08b948cc165efd4385e6388036568f..c4553f31f58a4d9442c087dddfd5a8636823c386 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/$Matrices.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/$Matrices.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/$Nat$Literals.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/$Nat$Literals.omdoc.xz index b90ce0538ce1ee6c60141d9933e3002ed48e60e6..1da4d3fe7390e3654cb3fbe8f4a19f096653234b 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/$Nat$Literals.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/$Nat$Literals.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/$Natural$Deduction.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/$Natural$Deduction.omdoc.xz index c85738b50a45b68fb8ae964fdf54512cc9d98dbc..cb24a1d2bc8d0eaeccf55def1ac59a7152f87c2a 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/$Natural$Deduction.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/$Natural$Deduction.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/$Option$Type.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/$Option$Type.omdoc.xz index 413d29e4d215c367176376a242f7739c09a59905..8e017d35bbd8af976be531e1c87944b264850f3e 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/$Option$Type.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/$Option$Type.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/$Sequences.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/$Sequences.omdoc.xz index 7f1cee45d4b141ba7cafdcd0130a2fd64a86a96e..0312b47acff070f0d1031992233605e406e8e9f0 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/$Sequences.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/$Sequences.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/Units/$Field.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/Units/$Field.omdoc.xz index 12dacb6408d4404337e4c249bfe9852dfd7d4967..9ecdfa3035a4a6548e03a7d524857f3871cc6439 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/Units/$Field.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/Units/$Field.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/Units/$S$I$Units.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/Units/$S$I$Units.omdoc.xz index a241a971076160533b3ea3a92a7e178aea021c89..5fec95b7253e47671bb17b02d7cd990657e16b13 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/Units/$S$I$Units.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/Units/$S$I$Units.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/Units/$Units$Extended.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/Units/$Units$Extended.omdoc.xz index 6fe0e8dd25749127fe2100cb2b8561da25eb458f..632793141bd9f32147b5baf7ed438cfa0b0599b5 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/Units/$Units$Extended.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/Units/$Units$Extended.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/Units/$Units.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/Units/$Units.omdoc.xz index 9b985a42b796d5035a67ba2209aa24437fcc7336..81f6b9fcd060d2a1b75d7a4d67c4292dc1bfc75a 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/Units/$Units.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/Units/$Units.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Binary$Union.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Binary$Union.omdoc.xz index 423045209ac791713901dd6eb39ae078c6760690..0846265b469f1fb77eecff9d90ad197a794b1dfa 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Binary$Union.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Binary$Union.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Cartesian$Product.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Cartesian$Product.omdoc.xz index 54d787357177cd81946e9ef56d7d73cb99ac99a6..3f9ea5286f26af6f82df999ad52fc3be50233191 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Cartesian$Product.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Cartesian$Product.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Choice.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Choice.omdoc.xz index 55ce25ae533537494c9bc48c86ff60c41d936266..8e78bdf4f51106911322454861d46c1aca5b3cdd 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Choice.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Choice.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Classes.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Classes.omdoc.xz index e31ee4a3a006f17f78ce2ddef2623fea64f7d3e1..8d9ead65da5287f36d8eff36e8ae8ed5ce496ebe 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Classes.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Classes.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Finite.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Finite.omdoc.xz index e39c123d061ca91eb2f7fe2a24239f6ec66a112d..eade4d859983c0ddd1b918a2d577e8c81a8464c6 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Finite.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Finite.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Functions$Extended.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Functions$Extended.omdoc.xz index e0ff3c8e3aab81a0996cc3a76ab183aa828e5ad3..4274c49499a428cf8636ffe78e07c77faf55a94b 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Functions$Extended.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Functions$Extended.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Functions.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Functions.omdoc.xz index b0911b34129631e1c60b5f87d2daa5ed245be9b4..70d4bbd29957043ba3cd7ab4168d9a957a70b050 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Functions.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Functions.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Infinity.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Infinity.omdoc.xz index 13059698c76d6c15472f91309a006bee022784cb..715f16c8dc0ffa2c5556a4c3192cd61049da488b 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Infinity.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Infinity.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Intersection.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Intersection.omdoc.xz index 4fdb4ba997d73867dbb1bce68e12e1930e0ac823..8ca6cf095be8b5d87cd9cedca179f2b8f54cb40c 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Intersection.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Intersection.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Kuratowski$Pairs.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Kuratowski$Pairs.omdoc.xz index c351db8bd8da9b9b9033cc13049bd2de973b4384..6bb20eaebb83d21f991f8991bf8228911fe75e21 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Kuratowski$Pairs.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Kuratowski$Pairs.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Omega.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Omega.omdoc.xz index 999b1f90186e02a9064e5f0f69514bf46af04ef8..e115e2e7b04f0742252ddee78bb62b71a89d3400 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Omega.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Omega.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Product.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Product.omdoc.xz index ccb27b74e2b14710fdf4b73d631acd9fdae0ad7b..9d06ee1375fa9f8a2cea041748714c57140efdf8 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Product.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Product.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Separation.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Separation.omdoc.xz index ba443f75c646b063dae915208c2db1470f0aaa4f..3d9ecdac9804986f3e9b556cd623084022e360fd 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Separation.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Lift$Separation.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Pairing.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Pairing.omdoc.xz index a2adec35b636d266726550b91e6f2511a4d19833..b1b4cc85119853602fc122015c230a616ad10577 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Pairing.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Pairing.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Powerset.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Powerset.omdoc.xz index ba2661851a5d9b42d6f0e634c6c60c207df95d31..59a4fbd4f5a50be99c8db0bca10a5572134f84dd 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Powerset.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Powerset.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Relations.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Relations.omdoc.xz index 51b2e6505375c09d2f4424eefdebc39b3758e060..b3979a4c19acfc9a591cc564ec5e3ec49389c297 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Relations.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Relations.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Replacement.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Replacement.omdoc.xz index 7ce4609bc916e3c1277ea1933d49ebd19d2e6811..586da2075b83aa6c6fe9dc80027c41fd7f20a680 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Replacement.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Replacement.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Separation.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Separation.omdoc.xz index 86b958d0476a5a97c972af366d32c4f966b3e529..6ee351521de057bc4c78ecd6db8f616e1b6ab6f8 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Separation.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Separation.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Set$Type$Conversions.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Set$Type$Conversions.omdoc.xz index 29574216c829d32dc11d7ff8abb62bfa09734a8a..a1def58cb4c14bde84b1752860de4be3af3cbd3d 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Set$Type$Conversions.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Set$Type$Conversions.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Sets.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Sets.omdoc.xz index 2d781a973dfa5d1eee3464ecc619229cfb6d25c5..6e52e42b62ee98bfdea569f98b1068c98476c010 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Sets.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Sets.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Typed$Sets.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Typed$Sets.omdoc.xz index 1c6093fca2294feb3951c2e44a4c609d185c0cca..21efe2249864d0e0644f19345682aeb216f33dce 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Typed$Sets.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Typed$Sets.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Union.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Union.omdoc.xz index 5e89f62eaa7a7fcf7a8d4ba35595d08b13edfaca..6ee01c786cc242feca40e9ebf69daccf42f3b97d 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Union.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Union.omdoc.xz differ diff --git a/content/http..mathhub.info/MitM/Foundation/sets/$Z$F.omdoc.xz b/content/http..mathhub.info/MitM/Foundation/sets/$Z$F.omdoc.xz index a2caca1cf4989d73e7cceb2cf9085ea9fb0ff23d..f6600b14951df6e1ecd204849ede4b175d559abe 100644 Binary files a/content/http..mathhub.info/MitM/Foundation/sets/$Z$F.omdoc.xz and b/content/http..mathhub.info/MitM/Foundation/sets/$Z$F.omdoc.xz differ diff --git a/relational/http..mathhub.info/MitM/Foundation/$Description$Operator.rel b/relational/http..mathhub.info/MitM/Foundation/$Description$Operator.rel index 15286328f1fb883cdf2d613df4e2dc5f15bf2905..138d6c2913a79fed23255f893d9d07ded186ea16 100644 --- a/relational/http..mathhub.info/MitM/Foundation/$Description$Operator.rel +++ b/relational/http..mathhub.info/MitM/Foundation/$Description$Operator.rel @@ -20,6 +20,7 @@ Declares http://mathhub.info/MitM/Foundation?DescriptionOperator http://mathhub. constant http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?DescriptionOperator?that?type +DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?eq?type DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?and?type DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://cds.omdoc.org/urtheories?Bool?BOOL?type DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?exists_unique?type @@ -28,7 +29,9 @@ DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?typ DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?exists?type DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?ded?definition DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?unique?type +DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?implies?type DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?prop?type +DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?forall?type DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?that_proof?type http://mathhub.info/MitM/Foundation?Logic?prop?definition Declares http://mathhub.info/MitM/Foundation?DescriptionOperator http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else_exists_proof constant http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else_exists_proof @@ -60,8 +63,10 @@ DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else?d DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else?definition http://mathhub.info/MitM/Foundation?Logic?exists?type DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else?definition http://mathhub.info/MitM/Foundation?Logic?unique?type +DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else?definition http://mathhub.info/MitM/Foundation?Logic?implies?type DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else?definition http://mathhub.info/MitM/Foundation?Logic?or?type +DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else?definition http://mathhub.info/MitM/Foundation?Logic?forall?type DependsOn http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition Declares http://mathhub.info/MitM/Foundation?DescriptionOperator http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else_case constant http://mathhub.info/MitM/Foundation?DescriptionOperator?if_then_else_case diff --git a/relational/http..mathhub.info/MitM/Foundation/$Natural$Deduction.rel b/relational/http..mathhub.info/MitM/Foundation/$Natural$Deduction.rel index 7b8faf156bd40def2ccac17678b432cda3edb30e..5d5474b48fc923722cb4169c81be5b24e11dde6b 100644 --- a/relational/http..mathhub.info/MitM/Foundation/$Natural$Deduction.rel +++ b/relational/http..mathhub.info/MitM/Foundation/$Natural$Deduction.rel @@ -34,12 +34,14 @@ DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?tru_introduction? DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?tru_introduction?type http://cds.omdoc.org/urtheories?Bool?BOOL?type DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?tru_introduction?type http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?tru_introduction?type http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?tru_introduction?type http://mathhub.info/MitM/Foundation?Logic?prop?definition Declares http://mathhub.info/MitM/Foundation?NaturalDeduction http://mathhub.info/MitM/Foundation?NaturalDeduction?fals_elimination constant http://mathhub.info/MitM/Foundation?NaturalDeduction?fals_elimination DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?fals_elimination?type http://mathhub.info/MitM/Foundation?Logic?ded?definition DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?fals_elimination?type http://cds.omdoc.org/urtheories?Bool?BOOL?type DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?fals_elimination?type http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?fals_elimination?type http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?fals_elimination?type http://mathhub.info/MitM/Foundation?Logic?prop?definition Declares http://mathhub.info/MitM/Foundation?NaturalDeduction http://mathhub.info/MitM/Foundation?NaturalDeduction?fals_introduction constant http://mathhub.info/MitM/Foundation?NaturalDeduction?fals_introduction DependsOn http://mathhub.info/MitM/Foundation?NaturalDeduction?fals_introduction?type http://mathhub.info/MitM/Foundation?Logic?not?type diff --git a/relational/http..mathhub.info/MitM/Foundation/$Trigonometry.rel b/relational/http..mathhub.info/MitM/Foundation/$Trigonometry.rel index 459549966be25a029b313bfd4237fbd3fdca020e..4fbf1c21694142d4a7b3c8624e08e2095cd2adc1 100644 --- a/relational/http..mathhub.info/MitM/Foundation/$Trigonometry.rel +++ b/relational/http..mathhub.info/MitM/Foundation/$Trigonometry.rel @@ -40,4 +40,3 @@ Declares http://mathhub.info/MitM/Foundation?Trigonometry http://mathhub.info/Mi constant http://mathhub.info/MitM/Foundation?Trigonometry?[scala://rules.mitm.mmt.kwarc.info?Acos] Declares http://mathhub.info/MitM/Foundation?Trigonometry http://mathhub.info/MitM/Foundation?Trigonometry?pi_num constant http://mathhub.info/MitM/Foundation?Trigonometry?pi_num -DependsOn http://mathhub.info/MitM/Foundation?Trigonometry?pi_num?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type diff --git a/relational/http..mathhub.info/MitM/Foundation/$Vectors.rel b/relational/http..mathhub.info/MitM/Foundation/$Vectors.rel index f1510cce8f78bae848acd7eae1f65f2010b4e36c..09cbe648d8952a7ce58f4ad47606628d261b6599 100644 --- a/relational/http..mathhub.info/MitM/Foundation/$Vectors.rel +++ b/relational/http..mathhub.info/MitM/Foundation/$Vectors.rel @@ -14,6 +14,7 @@ constant http://mathhub.info/MitM/Foundation?Vectors?zerovec DependsOn http://mathhub.info/MitM/Foundation?Vectors?zerovec?type http://cds.omdoc.org/urtheories?NatSymbols?NAT?type DependsOn http://mathhub.info/MitM/Foundation?Vectors?zerovec?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type DependsOn http://mathhub.info/MitM/Foundation?Vectors?zerovec?type http://mathhub.info/MitM/Foundation?Vectors?vector?type +DependsOn http://mathhub.info/MitM/Foundation?Vectors?zerovec?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition Declares http://mathhub.info/MitM/Foundation?Vectors http://mathhub.info/MitM/Foundation?Vectors?vector_prepend constant http://mathhub.info/MitM/Foundation?Vectors?vector_prepend DependsOn http://mathhub.info/MitM/Foundation?Vectors?vector_prepend?type http://cds.omdoc.org/urtheories?NatSymbols?NAT?type diff --git a/relational/http..mathhub.info/MitM/Foundation/sets/$Choice.rel b/relational/http..mathhub.info/MitM/Foundation/sets/$Choice.rel index 98a8bf216235916b221679c2d8079ebd12259301..a848945eb8a6df8c66b918081b55d562c6549c8b 100644 --- a/relational/http..mathhub.info/MitM/Foundation/sets/$Choice.rel +++ b/relational/http..mathhub.info/MitM/Foundation/sets/$Choice.rel @@ -37,7 +37,6 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Choice?prop_choiceFunction?de DependsOn http://mathhub.info/MitM/Foundation/sets?Choice?prop_choiceFunction?definition http://cds.omdoc.org/urtheories?Ded?DED?type DependsOn http://mathhub.info/MitM/Foundation/sets?Choice?prop_choiceFunction?definition http://mathhub.info/MitM/Foundation/sets?Powerset?axiom_powerset?type DependsOn http://mathhub.info/MitM/Foundation/sets?Choice?prop_choiceFunction?definition http://mathhub.info/MitM/Foundation/sets?Sets?subset?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Choice?prop_choiceFunction?definition http://mathhub.info/MitM/Foundation/sets?Functions?function?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Choice?prop_choiceFunction?definition http://mathhub.info/MitM/Foundation?Logic?exists?type DependsOn http://mathhub.info/MitM/Foundation/sets?Choice?prop_choiceFunction?definition http://mathhub.info/MitM/Foundation/sets?KuratowskiPairs?pair?type DependsOn http://mathhub.info/MitM/Foundation/sets?Choice?prop_choiceFunction?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition diff --git a/relational/http..mathhub.info/MitM/Foundation/sets/$Finite.rel b/relational/http..mathhub.info/MitM/Foundation/sets/$Finite.rel index b755d3b1e3a0740a3c421c1ba4e509fcaf877acf..8e6603b0807c8d52be5df7bdc098948d220cad95 100644 --- a/relational/http..mathhub.info/MitM/Foundation/sets/$Finite.rel +++ b/relational/http..mathhub.info/MitM/Foundation/sets/$Finite.rel @@ -17,6 +17,7 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Finite?prop_finite?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Finite?prop_finite?definition http://mathhub.info/MitM/Foundation/sets?Sets?prop_separation?type DependsOn http://mathhub.info/MitM/Foundation/sets?Finite?prop_finite?definition http://mathhub.info/MitM/Foundation/sets?Pairing?lemma_pairing_unique?type DependsOn http://mathhub.info/MitM/Foundation/sets?Finite?prop_finite?definition http://mathhub.info/MitM/Foundation/sets?Pairing?uopair?type +DependsOn http://mathhub.info/MitM/Foundation/sets?Finite?prop_finite?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type DependsOn http://mathhub.info/MitM/Foundation/sets?Finite?prop_finite?definition http://mathhub.info/MitM/Foundation?Logic?ded?type DependsOn http://mathhub.info/MitM/Foundation/sets?Finite?prop_finite?definition http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_injective?type DependsOn http://mathhub.info/MitM/Foundation/sets?Finite?prop_finite?definition http://mathhub.info/MitM/Foundation/sets?BinaryUnion?binaryunion?type diff --git a/relational/http..mathhub.info/MitM/Foundation/sets/$Functions$Extended.rel b/relational/http..mathhub.info/MitM/Foundation/sets/$Functions$Extended.rel index a52b9e18a09acabe803011ebf02aa25598a90b00..65bfea2442bd7dc9881ceee9306087dce6cbe326 100644 --- a/relational/http..mathhub.info/MitM/Foundation/sets/$Functions$Extended.rel +++ b/relational/http..mathhub.info/MitM/Foundation/sets/$Functions$Extended.rel @@ -20,6 +20,7 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_inject DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_injective?definition http://mathhub.info/MitM/Foundation/sets?Sets?prop_separation?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_injective?definition http://mathhub.info/MitM/Foundation/sets?Pairing?lemma_pairing_unique?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_injective?definition http://mathhub.info/MitM/Foundation/sets?Pairing?uopair?type +DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_injective?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_injective?definition http://mathhub.info/MitM/Foundation?Logic?ded?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_injective?definition http://mathhub.info/MitM/Foundation/sets?BinaryUnion?binaryunion?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_injective?definition http://mathhub.info/MitM/Foundation/sets?Functions?function?type @@ -65,6 +66,7 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_surjec DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_surjective?definition http://mathhub.info/MitM/Foundation/sets?Sets?prop_separation?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_surjective?definition http://mathhub.info/MitM/Foundation/sets?Pairing?lemma_pairing_unique?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_surjective?definition http://mathhub.info/MitM/Foundation/sets?Pairing?uopair?type +DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_surjective?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_surjective?definition http://mathhub.info/MitM/Foundation?Logic?ded?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_surjective?definition http://mathhub.info/MitM/Foundation/sets?BinaryUnion?binaryunion?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_surjective?definition http://mathhub.info/MitM/Foundation/sets?Functions?function?type @@ -109,6 +111,7 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_biject DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_bijective?definition http://mathhub.info/MitM/Foundation/sets?Sets?prop_separation?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_bijective?definition http://mathhub.info/MitM/Foundation/sets?Pairing?lemma_pairing_unique?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_bijective?definition http://mathhub.info/MitM/Foundation/sets?Pairing?uopair?type +DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_bijective?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_bijective?definition http://mathhub.info/MitM/Foundation?Logic?ded?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_bijective?definition http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_injective?type DependsOn http://mathhub.info/MitM/Foundation/sets?FunctionsExtended?prop_bijective?definition http://mathhub.info/MitM/Foundation/sets?BinaryUnion?binaryunion?type diff --git a/relational/http..mathhub.info/MitM/Foundation/sets/$Functions.rel b/relational/http..mathhub.info/MitM/Foundation/sets/$Functions.rel index 0d4cf230467b7b0b1d8d16e57057040bb22a9de8..460c4275157b2c8484188755c5cc413de29f6c07 100644 --- a/relational/http..mathhub.info/MitM/Foundation/sets/$Functions.rel +++ b/relational/http..mathhub.info/MitM/Foundation/sets/$Functions.rel @@ -14,7 +14,6 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?prop_function?defin DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?prop_function?definition http://mathhub.info/MitM/Foundation?Logic?implies?type DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?prop_function?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?prop_function?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?prop_function?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?prop_function?definition http://mathhub.info/MitM/Foundation?Logic?forall?type DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?prop_function?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition Declares http://mathhub.info/MitM/Foundation/sets?Functions http://mathhub.info/MitM/Foundation/sets?Functions?function @@ -56,6 +55,7 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?theorem_setfun?type DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?theorem_setfun?type http://mathhub.info/MitM/Foundation/sets?Sets?prop_separation?type DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?theorem_setfun?type http://mathhub.info/MitM/Foundation/sets?Pairing?lemma_pairing_unique?type DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?theorem_setfun?type http://mathhub.info/MitM/Foundation/sets?Pairing?uopair?type +DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?theorem_setfun?type http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?theorem_setfun?type http://mathhub.info/MitM/Foundation?Logic?ded?type DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?theorem_setfun?type http://mathhub.info/MitM/Foundation/sets?BinaryUnion?binaryunion?type DependsOn http://mathhub.info/MitM/Foundation/sets?Functions?theorem_setfun?type http://mathhub.info/MitM/Foundation/sets?Functions?function?type diff --git a/relational/http..mathhub.info/MitM/Foundation/sets/$Infinity.rel b/relational/http..mathhub.info/MitM/Foundation/sets/$Infinity.rel index 4b101f1319939f68d8fce6a045ccdfc59616ad26..5d2be62d43d8617029e8cd71d05aef08c635e24c 100644 --- a/relational/http..mathhub.info/MitM/Foundation/sets/$Infinity.rel +++ b/relational/http..mathhub.info/MitM/Foundation/sets/$Infinity.rel @@ -17,7 +17,6 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Infinity?prop_infinity?defini DependsOn http://mathhub.info/MitM/Foundation/sets?Infinity?prop_infinity?definition http://mathhub.info/MitM/Foundation?Logic?implies?type DependsOn http://mathhub.info/MitM/Foundation/sets?Infinity?prop_infinity?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Infinity?prop_infinity?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Infinity?prop_infinity?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation/sets?Infinity?prop_infinity?definition http://mathhub.info/MitM/Foundation?Logic?forall?type DependsOn http://mathhub.info/MitM/Foundation/sets?Infinity?prop_infinity?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition Declares http://mathhub.info/MitM/Foundation/sets?Infinity http://mathhub.info/MitM/Foundation/sets?Infinity?omega diff --git a/relational/http..mathhub.info/MitM/Foundation/sets/$Powerset.rel b/relational/http..mathhub.info/MitM/Foundation/sets/$Powerset.rel index ef838e74e00922a2da260804ab0edfbad3b3eb1f..f22ad6e9c4b63b1760fc25d60381111760c581a8 100644 --- a/relational/http..mathhub.info/MitM/Foundation/sets/$Powerset.rel +++ b/relational/http..mathhub.info/MitM/Foundation/sets/$Powerset.rel @@ -18,6 +18,7 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?type http:/ DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation/sets?Sets?prop_powerset?type DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation?DescriptionOperator?that?type +DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation?Logic?eq?type DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation?Logic?and?type DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation?Logic?ded?type @@ -27,6 +28,7 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation?Logic?exists?type DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation?Logic?unique?type +DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation?Logic?implies?type DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type DependsOn http://mathhub.info/MitM/Foundation/sets?Powerset?powerset?definition http://mathhub.info/MitM/Foundation?Logic?prop?type diff --git a/relational/http..mathhub.info/MitM/Foundation/sets/$Relations.rel b/relational/http..mathhub.info/MitM/Foundation/sets/$Relations.rel index ce36a07b7a2bdee26d85f086ce89b7a47ee1607f..f0911c0369265ef3d75e5b62dc02e1b8a6e95cf7 100644 --- a/relational/http..mathhub.info/MitM/Foundation/sets/$Relations.rel +++ b/relational/http..mathhub.info/MitM/Foundation/sets/$Relations.rel @@ -9,7 +9,6 @@ constant http://mathhub.info/MitM/Foundation/sets?Relations?prop_relation DependsOn http://mathhub.info/MitM/Foundation/sets?Relations?prop_relation?definition http://mathhub.info/MitM/Foundation/sets?Sets?subset?type DependsOn http://mathhub.info/MitM/Foundation/sets?Relations?prop_relation?definition http://mathhub.info/MitM/Foundation/sets?CartesianProduct?product?type DependsOn http://mathhub.info/MitM/Foundation/sets?Relations?prop_relation?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Relations?prop_relation?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation/sets?Relations?prop_relation?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition Declares http://mathhub.info/MitM/Foundation/sets?Relations http://mathhub.info/MitM/Foundation/sets?Relations?relation constant http://mathhub.info/MitM/Foundation/sets?Relations?relation diff --git a/relational/http..mathhub.info/MitM/Foundation/sets/$Separation.rel b/relational/http..mathhub.info/MitM/Foundation/sets/$Separation.rel index 0e3ee3006500188193eaa8de640b9e6cd4fdcacb..98ce6774a5700e45d198e55092f19ab951ec2660 100644 --- a/relational/http..mathhub.info/MitM/Foundation/sets/$Separation.rel +++ b/relational/http..mathhub.info/MitM/Foundation/sets/$Separation.rel @@ -20,6 +20,7 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?ty DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?type http://mathhub.info/MitM/Foundation?Logic?prop?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation?DescriptionOperator?that?type +DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation?Logic?eq?type DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation?Logic?and?type DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation/sets?Sets?prop_separation?type DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type @@ -29,6 +30,7 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?de DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation?Logic?exists?type DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation?Logic?unique?type +DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation?Logic?implies?type DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type DependsOn http://mathhub.info/MitM/Foundation/sets?Separation?sep_constructor?definition http://mathhub.info/MitM/Foundation?Logic?prop?type diff --git a/relational/http..mathhub.info/MitM/Foundation/sets/$Sets.rel b/relational/http..mathhub.info/MitM/Foundation/sets/$Sets.rel index 4ebc6580a227e3634a854ab1d7d133e8b726b39d..8a8218292c3edb2200e30f828b7668ed388e6fe1 100644 --- a/relational/http..mathhub.info/MitM/Foundation/sets/$Sets.rel +++ b/relational/http..mathhub.info/MitM/Foundation/sets/$Sets.rel @@ -82,7 +82,6 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_extensionality?defi DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_extensionality?definition http://mathhub.info/MitM/Foundation?Logic?implies?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_extensionality?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_extensionality?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_extensionality?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_extensionality?definition http://mathhub.info/MitM/Foundation?Logic?iff?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_extensionality?definition http://mathhub.info/MitM/Foundation?Logic?forall?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_extensionality?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition @@ -108,7 +107,6 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_regularity?definiti DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_regularity?definition http://mathhub.info/MitM/Foundation?Logic?neq?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_regularity?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_regularity?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_regularity?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_regularity?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition Declares http://mathhub.info/MitM/Foundation/sets?Sets http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing constant http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing @@ -116,7 +114,6 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing?definition http://mathhub.info/MitM/Foundation?Logic?and?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition Declares http://mathhub.info/MitM/Foundation/sets?Sets http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing_unique constant http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing_unique @@ -126,7 +123,6 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing_unique?defi DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing_unique?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing_unique?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing_unique?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing_unique?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing_unique?definition http://mathhub.info/MitM/Foundation?Logic?or?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing_unique?definition http://mathhub.info/MitM/Foundation?Logic?forall?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_pairing_unique?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition @@ -137,7 +133,6 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_union?definition ht DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_union?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_union?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_union?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_union?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_union?definition http://mathhub.info/MitM/Foundation?Logic?iff?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_union?definition http://mathhub.info/MitM/Foundation?Logic?forall?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_union?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition @@ -147,7 +142,6 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_powerset?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_powerset?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_powerset?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_powerset?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_powerset?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_powerset?definition http://mathhub.info/MitM/Foundation?Logic?iff?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_powerset?definition http://mathhub.info/MitM/Foundation?Logic?forall?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_powerset?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition @@ -158,7 +152,6 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_replacement?definit DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_replacement?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_replacement?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_replacement?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type -DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_replacement?definition http://mathhub.info/MitM/Foundation?Logic?prop?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_replacement?definition http://mathhub.info/MitM/Foundation?Logic?iff?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_replacement?definition http://mathhub.info/MitM/Foundation?Logic?forall?type DependsOn http://mathhub.info/MitM/Foundation/sets?Sets?prop_replacement?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition diff --git a/relational/http..mathhub.info/MitM/Foundation/sets/$Union.rel b/relational/http..mathhub.info/MitM/Foundation/sets/$Union.rel index 4b6663af34eb41769fdac12550ae46f865a82eb6..36cc9df54b0aea55dabf4b7e54592802987d643c 100644 --- a/relational/http..mathhub.info/MitM/Foundation/sets/$Union.rel +++ b/relational/http..mathhub.info/MitM/Foundation/sets/$Union.rel @@ -17,6 +17,7 @@ constant http://mathhub.info/MitM/Foundation/sets?Union?union DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?type http://mathhub.info/MitM/Foundation/sets?Sets?set?type DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation?DescriptionOperator?that?type +DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation?Logic?eq?type DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation/sets?Union?axiom_union?type DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation?Logic?and?type DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type @@ -26,6 +27,7 @@ DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http:/ DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation?Logic?exists?type DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation?Logic?unique?type +DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation?Logic?implies?type DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation/sets?Sets?element?type DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation/sets?Sets?set?type DependsOn http://mathhub.info/MitM/Foundation/sets?Union?union?definition http://mathhub.info/MitM/Foundation?Logic?prop?type