The place to suggest improvements and revisions to existing MML articles. ** NOTE:** Start a new topic for each idea.

Suggestion: Revising FINSEQ 1:20 FINSEQ 1:20 is a nice little minitheorem on composing finite sequences with other functions: for f being Function for p being FinSequence ...

Suggestion: Revising MATRLIN:20 MATRLIN:20 is the theorem for K being Field for V2, V1 being finite dimensional VectSp of K for f being Function of V1,V2 for p being ...

Suggestion: Use expandable mode definition of Field In VECTSP 1, I find the reservation block: reserve F for Field, x for Element of F, V for ...

Suggestion: Partial unions, intersections, etc. See attached file. GrzegorzBancerek 04 Jan 2006 Article name: MML version: Follow ...

Suggestion: sigma Field of Subsets Two introductions of one concept, SigmaField from PROB 1 and sigma Field Subset from MEASURE1, should be unified. GrzegorzBancerek ...

Suggestion: Meet for functions In FUNCT 6:def 4 to omit problems with identification change meet f Meet f In PROB 1:def 5 and PROB 3:def 9 Intersection should ...

Suggestion: Revising the proof of Gödel's Completeness Theorem I would like to propose some changes to GOEDELCP, which contains a proof of Gödel's completeness theorem ...

FunctorResultClusters There seems to be some redundancy in clusters for f.x see FUNCT 1:func.1 funcreg Follow up

Suggestion: TopRealAsSynonym Replace EUCLID:def.8 with a synonym TOP REAL n for nop TopSpaceMetr (Euclid n) the strictness is then automatic, the nop TopSpace ...

Suggestion: RLVECT into NAT 1 Move theorems about naturals from RLVECT 1 and RLVECT 2 to NAT 1 before NAT 1:18. Follow up RLVECT 1: RLVECT 1:th.98 RLVECT 1:th.99 ...

Suggestion: Rename the attribute "connected" We have definition let L be non empty RelStr; attr L is connected means :: WAYBEL 0:def 29 for x,y being Element ...

Suggestion: Casting theorem for integers I did not find st. like i0 is Nat iff ex n being Nat st n theorem :: INT 1:16 0 Article name: INT 1 ...

Suggestion: Interface between Relations and Graphs It would be nice to have an easy transition between the notions and theorems written in MML for graphs and those ...

Number of topics: 13

-- JosefUrban - 10 Jul 2002

Edit | Attach | Print version | History: r1 | Backlinks | Raw View | Raw edit | More topic actions

Topic revision: r1 - 2002-07-10 - 09:42:00 - JosefUrban

Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.

Ideas, requests, problems regarding TWiki? Send feedback

Ideas, requests, problems regarding TWiki? Send feedback