felix.git/library/numbers.tex, branch hotg Unnamed repository; edit this file 'description' to name the repository. https://git.adelon.net/felix.git/atom?h=hotg 2025-11-27T18:44:07+00:00 Update errors and cull formalizations 2025-11-27T18:44:07+00:00 adelon 22380201+adelon@users.noreply.github.com 2025-11-27T18:44:07+00:00 urn:sha1:aa760e1989ccc2c7e45b6a3f111e5d5d3bc713b3 Linting 2025-07-08T14:05:16+00:00 adelon 22380201+adelon@users.noreply.github.com 2025-07-08T14:05:16+00:00 urn:sha1:db353b6d19eb5cb4181b64fe37a1bd550395169c Abgabe 2024-09-23T01:05:41+00:00 Simon-Kor 52245124+Simon-Kor@users.noreply.github.com 2024-09-23T01:05:41+00:00 urn:sha1:f6b22fd533bd61e9dbcb6374295df321de99b1f2 Corrected Math Env Parsing 2024-09-16T22:36:24+00:00 Simon-Kor 52245124+Simon-Kor@users.noreply.github.com 2024-09-16T22:36:24+00:00 urn:sha1:5362771c14eccd80fd1a3ab6521c3a6ad9bb7838 Since Latex has a really specify syntax for \begin{cases} ... \end{cases} The math mode in tokenizing had to be setup correctly. Topo Space Real Verfication 2024-09-16T21:24:08+00:00 Simon-Kor 52245124+Simon-Kor@users.noreply.github.com 2024-09-16T21:24:08+00:00 urn:sha1:3dca719ba8f9a59471f2c761cf8846cf597eae97 working commit 2024-09-16T17:37:27+00:00 Simon-Kor 52245124+Simon-Kor@users.noreply.github.com 2024-09-16T17:37:27+00:00 urn:sha1:c021e79033abbb3fd4458304e701b3c54a284902 Finished proof of topological basis 2024-09-16T14:19:36+00:00 Simon-Kor 52245124+Simon-Kor@users.noreply.github.com 2024-09-16T14:19:36+00:00 urn:sha1:13d7b11c23f8862c9f214c46ee05fad314e9e698 Fix Assume Issue 2024-09-15T17:05:25+00:00 Simon-Kor 52245124+Simon-Kor@users.noreply.github.com 2024-09-15T17:05:25+00:00 urn:sha1:3ef20da08eda23db76d763a2c6c7ee416348a021 At line 137 in real-topological-space.tex Can't use Fix at this point. Issue at Fixing. 2024-09-15T13:07:36+00:00 Simon-Kor 52245124+Simon-Kor@users.noreply.github.com 2024-09-15T13:07:36+00:00 urn:sha1:b298295ac002785672a8b16dd09f9692d73f7a80 In Line 49 in real-topological-space.tex the Fix can't be processed. Mismatched Assume in Induction 2024-09-04T13:17:50+00:00 Simon-Kor 52245124+Simon-Kor@users.noreply.github.com 2024-09-04T13:17:50+00:00 urn:sha1:68716d1ab46dee3dfc1b03089f941dbb6883cdcd Unexpeced Mismatch in line 99 and 109 or the pair 100 and 108. Parsing works with line 99 and 108 or with the lines 100 and 109. zf: MismatchedAssume (TermSymbol (SymbolPredicate (PredicateNoun (SgPl {sg = [Just (Word "natural"),Just (Word "number")], pl = [Just (Word "natural"),Just (Word "numbers")]}))) [TermVar (NamedVar "n")]) (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (NamedVar "n"),TermSymbol (SymbolMixfix [Just (Command "naturals")]) []]) (TermSymbol (SymbolPredicate (PredicateVerb (SgPl {sg = [Just (Word "has"),Just (Word "cardinality"),Nothing], pl = [Just (Word "ha"),Just (Word "cardinality"),Nothing]}))) [TermSymbol (SymbolMixfix [Just (Command "seq"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR,Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermSymbol (SymbolMixfix [Just (Command "emptyset")]) [],TermVar (NamedVar "n")],TermSymbol (SymbolMixfix [Just (Command "suc"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermVar (NamedVar "n")]]))