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 VectSp-like add-associative ...
Suggestion: sigma Field of Subsets Two introductions of one concept, SigmaField from PROB 1 and sigma Field Subset from MEASURE1, should be unified. Main.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 be ...
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 ...
Suggestion: TopRealAsSynonym Replace QMEANING EUCLID:def.8 with a synonym TOP-REAL n for TopSpaceMetr (Euclid n) the strictness is then automatic, the TopSpace can ...
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: QMEANING RLVECT 1:th.98 QMEANING ...
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 of L ...
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 ...