Commit b97b5d83 authored by Dennis Müller's avatar Dennis Müller

generated files

parent 3044d7da
This diff is collapsed.
<errors>
<error target="object-parser" sref="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#1799.54.104:1804.54.109" type="info.kwarc.mmt.api.SourceError" shortMsg="unbound token: degree" level="2">
source error (object-parser) at http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#1799.54.104:1804.54.109
<stacktrace>
<element>info.kwarc.mmt.api.parser.NotationBasedParser.makeError(NotationBasedParser.scala:94)</element>
<element>info.kwarc.mmt.api.parser.NotationBasedParser.makeTerm(NotationBasedParser.scala:322)</element>
<element>info.kwarc.mmt.api.parser.NotationBasedParser.makeTerm(NotationBasedParser.scala:336)</element>
<element>info.kwarc.mmt.api.parser.NotationBasedParser.$anonfun$apply$10(NotationBasedParser.scala:215)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.NotationBasedParser.logGroup(NotationBasedParser.scala:69)</element>
<element>info.kwarc.mmt.api.parser.NotationBasedParser.apply(NotationBasedParser.scala:215)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.puCont(StructureParser.scala:149)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readParsedObject(StructureParser.scala:295)</element>
<element>info.kwarc.mmt.api.parser.MetadataParser$.apply(MetaData.scala:32)</element>
<element>info.kwarc.mmt.api.parser.MetadataParser$.apply(MetaData.scala:13)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readConstant(StructureParser.scala:902)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:635)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:462)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:715)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:715)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:410)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:186)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:186)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:176)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:93)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:134)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
</errors>
......@@ -35,7 +35,33 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid un
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:134)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
<element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:122)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:121)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
<element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:100)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:77)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:77)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:76)</element>
<element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:73)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:47)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:35)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:73)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:31)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:29)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:73)</element>
<element>Test.hl(preamble.scala:98)</element>
<element>Debug$.$anonfun$buildSmglom$1(Debug.scala:165)</element>
<element>Debug$.$anonfun$buildSmglom$1$adapted(Debug.scala:165)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>Debug$.buildSmglom(Debug.scala:165)</element>
<element>Debug$.run(Debug.scala:113)</element>
<element>Test.main(preamble.scala:78)</element>
<element>Debug.main(Debug.scala)</element>
</stacktrace>
</error>
......@@ -75,7 +101,33 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid un
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:134)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
<element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:122)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:121)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
<element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:100)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:77)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:77)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:76)</element>
<element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:73)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:47)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:35)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:73)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:31)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:29)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:73)</element>
<element>Test.hl(preamble.scala:98)</element>
<element>Debug$.$anonfun$buildSmglom$1(Debug.scala:165)</element>
<element>Debug$.$anonfun$buildSmglom$1$adapted(Debug.scala:165)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>Debug$.buildSmglom(Debug.scala:165)</element>
<element>Debug$.run(Debug.scala:113)</element>
<element>Test.main(preamble.scala:78)</element>
<element>Debug.main(Debug.scala)</element>
</stacktrace>
</error>
......@@ -115,7 +167,33 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid un
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:134)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
<element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:122)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:121)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
<element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:100)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:77)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:77)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:76)</element>
<element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:73)</element>
<element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:47)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:35)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:73)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:31)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:29)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:73)</element>
<element>Test.hl(preamble.scala:98)</element>
<element>Debug$.$anonfun$buildSmglom$1(Debug.scala:165)</element>
<element>Debug$.$anonfun$buildSmglom$1$adapted(Debug.scala:165)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>Debug$.buildSmglom(Debug.scala:165)</element>
<element>Debug$.run(Debug.scala:113)</element>
<element>Test.main(preamble.scala:78)</element>
<element>Debug.main(Debug.scala)</element>
</stacktrace>
</error>
......
<errors>
<error type="info.kwarc.mmt.api.InvalidUnit" shortMsg="invalid unit: http://mathhub.info/MitM/smglom/elliptic_curves?Weierstrass_model?polynomial_equation?type: Judgment |- weierstrass_model⟶polynomial INHABITABLE" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:104)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:102)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$14(RuleBasedChecker.scala:102)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:91)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:249)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$14(MMTStructureChecker.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$14$adapted(MMTStructureChecker.scala:254)</element>
<element>scala.Option.foreach(Option.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:254)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:72)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:87)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:99)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:484)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:636)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:462)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:715)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:715)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:410)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:186)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:186)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:176)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:93)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:134)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
<error
type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/MitM/smglom/elliptic_curves?Weierstrass_model?polynomial_equation_injectivity?type: Judgment |- {A,B}⊦(polynomial_equation A)≐(polynomial_equation B)⟶⊦A≐B INHABITABLE" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$16(RuleBasedChecker.scala:95)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$16$adapted(RuleBasedChecker.scala:94)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$14(RuleBasedChecker.scala:94)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:91)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:249)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$14(MMTStructureChecker.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$14$adapted(MMTStructureChecker.scala:254)</element>
<element>scala.Option.foreach(Option.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:254)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:72)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:87)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:99)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:484)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:636)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:462)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:715)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:715)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:410)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:186)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:186)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:176)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:93)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:134)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
</errors>
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/basics.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#0.0.0:5782.169.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra?OperationProps]" target="http://mathhub.info/MitM/smglom/algebra?OperationProps"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#264.6.0:284.6.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Magma]" target="http://mathhub.info/MitM/smglom/algebra?Magma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#1591.20.0:1602.20.11"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?SemiGroup]" target="http://mathhub.info/MitM/smglom/algebra?SemiGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2020.32.0:2035.32.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Unital]" target="http://mathhub.info/MitM/smglom/algebra?Unital"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2234.42.0:2246.42.12"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?QuasiGroup]" target="http://mathhub.info/MitM/smglom/algebra?QuasiGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2579.56.0:2595.56.16"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?CancellativeMagma]" target="http://mathhub.info/MitM/smglom/algebra?CancellativeMagma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3079.72.0:3102.72.23"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3599.88.0:3647.88.48"/></metadata>Refactor: a Loop is just a unital Quasigroup</opaque><mref name="[http://mathhub.info/MitM/smglom/algebra?Loop]" target="http://mathhub.info/MitM/smglom/algebra?Loop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3649.89.0:3659.89.10"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Monoid]" target="http://mathhub.info/MitM/smglom/algebra?Monoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4239.108.0:4251.108.12"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Group]" target="http://mathhub.info/MitM/smglom/algebra?Group"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4463.120.0:4474.120.11"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?AbelianGroup]" target="http://mathhub.info/MitM/smglom/algebra?AbelianGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5178.147.0:5196.147.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?GroupHomomorphism]" target="http://mathhub.info/MitM/smglom/algebra?GroupHomomorphism"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5428.158.0:5451.158.23"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/algebra/basics.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#0.0.0:5804.170.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra?OperationProps]" target="http://mathhub.info/MitM/smglom/algebra?OperationProps"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#264.6.0:284.6.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Magma]" target="http://mathhub.info/MitM/smglom/algebra?Magma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#1591.20.0:1602.20.11"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?SemiGroup]" target="http://mathhub.info/MitM/smglom/algebra?SemiGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2020.32.0:2035.32.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Unital]" target="http://mathhub.info/MitM/smglom/algebra?Unital"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2234.42.0:2246.42.12"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?QuasiGroup]" target="http://mathhub.info/MitM/smglom/algebra?QuasiGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2579.56.0:2595.56.16"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?CancellativeMagma]" target="http://mathhub.info/MitM/smglom/algebra?CancellativeMagma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3079.72.0:3102.72.23"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3599.88.0:3647.88.48"/></metadata>Refactor: a Loop is just a unital Quasigroup</opaque><mref name="[http://mathhub.info/MitM/smglom/algebra?Loop]" target="http://mathhub.info/MitM/smglom/algebra?Loop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3649.89.0:3659.89.10"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Monoid]" target="http://mathhub.info/MitM/smglom/algebra?Monoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4239.108.0:4251.108.12"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Group]" target="http://mathhub.info/MitM/smglom/algebra?Group"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4463.120.0:4474.120.11"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?AbelianGroup]" target="http://mathhub.info/MitM/smglom/algebra?AbelianGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5200.148.0:5218.148.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?GroupHomomorphism]" target="http://mathhub.info/MitM/smglom/algebra?GroupHomomorphism"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5450.159.0:5473.159.23"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/lattice.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#0.0.0:4463.125.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra?SemiLattice]" target="http://mathhub.info/MitM/smglom/algebra?SemiLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#157.4.0:174.4.17"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#1364.38.0:1822.48.0"/></metadata>MiKo: probably need to say that the meet order is the same as the join-order, i.e.
<omdoc base="http://mathhub.info/MitM/smglom/algebra/lattice.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#0.0.0:4419.126.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra?SemiLattice]" target="http://mathhub.info/MitM/smglom/algebra?SemiLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#157.4.0:174.4.17"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#1364.38.0:1822.48.0"/></metadata>MiKo: probably need to say that the meet order is the same as the join-order, i.e.
in theory SemiLattice/semilattice_theory
biviewMeet : ⊢ SemilatticeIsPOSet (POSetIsMeetSemiLattice op ) ≐ op
biviewJoin : ⊢ SemilatticeIsPOSet (POSetIsJoinSemiLattice op ) ≐ op
......@@ -8,4 +8,4 @@ in theory SemiLattice/semilattice_theory
theory ts:?POSet/poset_theory
biviewMeet : ⊢ POSetIsMeetSemiLattice (SemilatticeIsPOSet ord ) ≐ ord
biviewMeet : ⊢ POSetIsMeetSemiLattice (SemilatticeIsPOSet ord ) ≐ ord</opaque><mref name="[http://mathhub.info/MitM/smglom/algebra?Lattice]" target="http://mathhub.info/MitM/smglom/algebra?Lattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#1825.50.0:1838.50.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?DistributiveLattice]" target="http://mathhub.info/MitM/smglom/algebra?DistributiveLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#2949.80.0:2974.80.25"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?BoundedLattice]" target="http://mathhub.info/MitM/smglom/algebra?BoundedLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3321.94.0:3341.94.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?ComplementedLattice]" target="http://mathhub.info/MitM/smglom/algebra?ComplementedLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3704.107.0:3729.107.25"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra]" target="http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4148.118.0:4168.118.20"/></metadata></mref></omdoc>
\ No newline at end of file
biviewMeet : ⊢ POSetIsMeetSemiLattice (SemilatticeIsPOSet ord ) ≐ ord</opaque><mref name="[http://mathhub.info/MitM/smglom/algebra?Lattice]" target="http://mathhub.info/MitM/smglom/algebra?Lattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#1825.50.0:1838.50.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?DistributiveLattice]" target="http://mathhub.info/MitM/smglom/algebra?DistributiveLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#2979.81.0:3004.81.25"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?BoundedLattice]" target="http://mathhub.info/MitM/smglom/algebra?BoundedLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3331.95.0:3351.95.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?ComplementedLattice]" target="http://mathhub.info/MitM/smglom/algebra?ComplementedLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3700.108.0:3725.108.25"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra]" target="http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4124.119.0:4144.119.20"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/permutation-group.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#0.0.0:1893.56.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra/permutationgroup?Permutations]" target="http://mathhub.info/MitM/smglom/algebra/permutationgroup?Permutations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#233.6.0:251.6.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/permutationgroup?GroupAction]" target="http://mathhub.info/MitM/smglom/algebra/permutationgroup?GroupAction"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#406.14.0:423.14.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/permutationgroup?PermutationGroup]" target="http://mathhub.info/MitM/smglom/algebra/permutationgroup?PermutationGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#924.29.0:946.29.22"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/permutationgroup?TransitiveGroupAction]" target="http://mathhub.info/MitM/smglom/algebra/permutationgroup?TransitiveGroupAction"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#1355.44.0:1382.44.27"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/algebra/permutation-group.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#0.0.0:1954.59.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra/permutationgroup?Permutations]" target="http://mathhub.info/MitM/smglom/algebra/permutationgroup?Permutations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#233.6.0:251.6.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/permutationgroup?GroupAction]" target="http://mathhub.info/MitM/smglom/algebra/permutationgroup?GroupAction"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#406.14.0:423.14.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/permutationgroup?PermutationGroup]" target="http://mathhub.info/MitM/smglom/algebra/permutationgroup?PermutationGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#944.31.0:966.31.22"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/permutationgroup?TransitiveGroupAction]" target="http://mathhub.info/MitM/smglom/algebra/permutationgroup?TransitiveGroupAction"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/permutation-group.mmt#1416.47.0:1443.47.27"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/polynomials.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/polynomials.mmt#0.0.0:1467.39.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra?Polynomials]" target="http://mathhub.info/MitM/smglom/algebra?Polynomials"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/polynomials.mmt#104.4.0:121.4.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?NumberSpaces]" target="http://mathhub.info/MitM/smglom/algebra?NumberSpaces"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/polynomials.mmt#927.22.0:945.22.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?RationalPolynomials]" target="http://mathhub.info/MitM/smglom/algebra?RationalPolynomials"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/polynomials.mmt#1071.29.0:1096.29.25"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/algebra/polynomials.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/polynomials.mmt#0.0.0:1500.41.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra?Polynomials]" target="http://mathhub.info/MitM/smglom/algebra?Polynomials"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/polynomials.mmt#104.4.0:121.4.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?NumberSpaces]" target="http://mathhub.info/MitM/smglom/algebra?NumberSpaces"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/polynomials.mmt#928.22.0:946.22.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?RationalPolynomials]" target="http://mathhub.info/MitM/smglom/algebra?RationalPolynomials"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/polynomials.mmt#1083.29.0:1108.29.25"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/elliptic_curves/Weierstrass-model.omf.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/elliptic_curves/Weierstrass-model.omf.mmt#0.0.0:1153.20.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/elliptic_curves?Weierstrass_model]" target="http://mathhub.info/MitM/smglom/elliptic_curves?Weierstrass_model"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/elliptic_curves/Weierstrass-model.omf.mmt#61.2.0:84.2.23"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/elliptic_curves/Weierstrass-model.omf.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/elliptic_curves/Weierstrass-model.omf.mmt#0.0.0:1169.20.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/elliptic_curves?Weierstrass_model]" target="http://mathhub.info/MitM/smglom/elliptic_curves?Weierstrass_model"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/elliptic_curves/Weierstrass-model.omf.mmt#61.2.0:84.2.23"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/functional-analysis/norms.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/functional-analysis/norms.mmt#0.0.0:2572.64.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/functional-analysis?NormedSpace]" target="http://mathhub.info/MitM/smglom/functional-analysis?NormedSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/functional-analysis/norms.mmt#346.8.0:363.8.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/functional-analysis?BanachSpace]" target="http://mathhub.info/MitM/smglom/functional-analysis?BanachSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/functional-analysis/norms.mmt#1551.34.0:1568.34.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/functional-analysis?BanachAlgebra]" target="http://mathhub.info/MitM/smglom/functional-analysis?BanachAlgebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/functional-analysis/norms.mmt#1957.47.0:1976.47.19"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/sets/filter.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/filter.mmt#0.0.0:948.19.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/typedsets?UpDownSet]" target="http://mathhub.info/MitM/smglom/typedsets?UpDownSet"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/filter.mmt#154.4.0:169.4.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/typedsets?filter]" target="http://mathhub.info/MitM/smglom/typedsets?filter"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/filter.mmt#437.10.0:449.10.12"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/sets/poset.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#0.0.0:3229.70.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/typedsets?PrOSet]" target="http://mathhub.info/MitM/smglom/typedsets?PrOSet"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#105.3.0:117.3.12"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/typedsets?LeastMost]" target="http://mathhub.info/MitM/smglom/typedsets?LeastMost"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#1081.26.0:1096.26.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/typedsets?DirectedSet]" target="http://mathhub.info/MitM/smglom/typedsets?DirectedSet"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#1684.37.0:1701.37.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/typedsets?POSet]" target="http://mathhub.info/MitM/smglom/typedsets?POSet"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#2814.60.0:2825.60.11"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/sets/poset.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#0.0.0:3852.81.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://mathhub.info/MitM/smglom/typedsets?PrOSet]" target="http://mathhub.info/MitM/smglom/typedsets?PrOSet"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#105.3.0:117.3.12"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/typedsets?LeastMost]" target="http://mathhub.info/MitM/smglom/typedsets?LeastMost"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#1081.26.0:1096.26.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/typedsets?DirectedSet]" target="http://mathhub.info/MitM/smglom/typedsets?DirectedSet"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#2106.42.0:2123.42.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/typedsets?Fixpoints]" target="http://mathhub.info/MitM/smglom/typedsets?Fixpoints"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#3236.65.0:3251.65.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/typedsets?POSet]" target="http://mathhub.info/MitM/smglom/typedsets?POSet"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/poset.mmt#3437.71.0:3448.71.11"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/sets/posetPowerset.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/posetPowerset.mmt#0.0.0:702.23.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/posetPowerset.mmt#105.3.0:279.5.33"/></metadata>MiKo: a first-order approximation of a view from POSet to PowerSet
eventually, we want to push filter and co out over this to get the
usual applications of filters</opaque><mref name="[http://mathhub.info/MitM/smglom/typedsets?ASet]" target="http://mathhub.info/MitM/smglom/typedsets?ASet"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/posetPowerset.mmt#282.7.0:292.7.10"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/typedsets?PowersetPOSet]" target="http://mathhub.info/MitM/smglom/typedsets?PowersetPOSet"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/sets/posetPowerset.mmt#378.13.0:397.13.19"/></metadata></mref></omdoc>
\ No newline at end of file
document http://mathhub.info/MitM/smglom/functional-analysis/norms.omdoc
Declares http://mathhub.info/MitM/smglom/functional-analysis/norms.omdoc http://mathhub.info/MitM/smglom/functional-analysis?NormedSpace
Declares http://mathhub.info/MitM/smglom/functional-analysis/norms.omdoc http://mathhub.info/MitM/smglom/functional-analysis?BanachSpace
Declares http://mathhub.info/MitM/smglom/functional-analysis/norms.omdoc http://mathhub.info/MitM/smglom/functional-analysis?BanachAlgebra
......@@ -10,8 +10,6 @@ Includes http://mathhub.info/MitM/smglom/algebra?AbelianGroup http://mathhub.inf
Includes http://mathhub.info/MitM/smglom/algebra?AbelianGroup http://mathhub.info/MitM/Foundation?DescriptionOperator
Includes http://mathhub.info/MitM/smglom/algebra?AbelianGroup http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/algebra?AbelianGroup http://mathhub.info/MitM/smglom/algebra?Loop
Includes http://mathhub.info/MitM/smglom/algebra?AbelianGroup http://gl.mathhub.info/MMT/LFX/Subtyping?SubSymbol
Includes http://mathhub.info/MitM/smglom/algebra?AbelianGroup http://gl.mathhub.info/MMT/LFX/Subtyping?SubRules
Includes http://mathhub.info/MitM/smglom/algebra?AbelianGroup http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentSymbol
Includes http://mathhub.info/MitM/smglom/algebra?AbelianGroup http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentRules
Includes http://mathhub.info/MitM/smglom/algebra?AbelianGroup http://gl.mathhub.info/MMT/LFX/Subtyping?PredSubSymbols
......
dataconstructor http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra?booleanalgebra
highuniverse http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra?booleanalgebra
theory http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra
HasMeta http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/Foundation?Strings
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/Foundation?InformalProofs
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://gl.mathhub.info/MMT/LFX/Subtyping?SubSymbol
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://gl.mathhub.info/MMT/LFX/Subtyping?SubRules
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentSymbol
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentRules
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://gl.mathhub.info/MMT/LFX/Subtyping?PredSubSymbols
......@@ -55,11 +53,10 @@ Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.i
Declares http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra?booleanAlgebra_theory
theory http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra/booleanAlgebra_theory
HasMeta http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra/booleanAlgebra_theory http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra/booleanAlgebra_theory http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra/booleanAlgebra_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra/booleanAlgebra_theory http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra/booleanAlgebra_theory http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complementedLattice_theory
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra/booleanAlgebra_theory http://mathhub.info/MitM/smglom/algebra?DistributiveLattice/distributiveLattice_theory
Declares http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra?booleanalgebra
constant http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra?booleanalgebra
Declares http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra?booleanalgebra/abbreviation
constant http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra?booleanalgebra/abbreviation
dataconstructor http://mathhub.info/MitM/smglom/algebra?BoundedLattice?boundedLattice
highuniverse http://mathhub.info/MitM/smglom/algebra?BoundedLattice?boundedLattice
theory http://mathhub.info/MitM/smglom/algebra?BoundedLattice
HasMeta http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/Foundation?Strings
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/Foundation?InformalProofs
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://gl.mathhub.info/MMT/LFX/Subtyping?SubSymbol
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://gl.mathhub.info/MMT/LFX/Subtyping?SubRules
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentSymbol
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentRules
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://gl.mathhub.info/MMT/LFX/Subtyping?PredSubSymbols
......@@ -53,16 +51,11 @@ Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.i
Declares http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/smglom/algebra?BoundedLattice?boundedLattice_theory
theory http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory
HasMeta http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory
Declares http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory?top
constant http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory?top
Declares http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory?bot
constant http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory?bot
Declares http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory?axiom_top
constant http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory?axiom_top
Declares http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory?axiom_bot
constant http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory?axiom_bot
Declares http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/smglom/algebra?BoundedLattice?boundedLattice
constant http://mathhub.info/MitM/smglom/algebra?BoundedLattice?boundedLattice
Declares http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/smglom/algebra?BoundedLattice?boundedLattice/abbreviation
constant http://mathhub.info/MitM/smglom/algebra?BoundedLattice?boundedLattice/abbreviation
dataconstructor http://mathhub.info/MitM/smglom/algebra?ComplementedLattice?complementedLattice
highuniverse http://mathhub.info/MitM/smglom/algebra?ComplementedLattice?complementedLattice
theory http://mathhub.info/MitM/smglom/algebra?ComplementedLattice
HasMeta http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/Foundation?Strings
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/Foundation?InformalProofs
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://gl.mathhub.info/MMT/LFX/Subtyping?SubSymbol
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://gl.mathhub.info/MMT/LFX/Subtyping?SubRules
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentSymbol
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentRules
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://gl.mathhub.info/MMT/LFX/Subtyping?PredSubSymbols
......@@ -54,6 +52,7 @@ Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://math
Declares http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/smglom/algebra?ComplementedLattice?complementedLattice_theory
theory http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complementedLattice_theory
HasMeta http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complementedLattice_theory http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complementedLattice_theory http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complementedLattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complementedLattice_theory http://mathhub.info/MitM/smglom/algebra?BoundedLattice/boundedLattice_theory
Declares http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complementedLattice_theory http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complementedLattice_theory?complement
......@@ -64,5 +63,3 @@ Declares http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complemente
constant http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complementedLattice_theory?axiom_complemented
Declares http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/smglom/algebra?ComplementedLattice?complementedLattice
constant http://mathhub.info/MitM/smglom/algebra?ComplementedLattice?complementedLattice
Declares http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/smglom/algebra?ComplementedLattice?complementedLattice/abbreviation
constant http://mathhub.info/MitM/smglom/algebra?ComplementedLattice?complementedLattice/abbreviation