Proposed changes to existing MML articles

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

New brainstorming topic (use a WikiWord title):

Results from Mizar web retrieved at 07:14 (GMT)

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

Topic revision: r1 - 2002-07-10 - 09:42:00 - JosefUrban
Mizar.MmlSuggestion moved from Mizar.MmlSuggestions on 2002-07-10 - 09:38 by JosefUrban - put it back
 
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback