Tämä dokumentti on eräänlainen luuranko Olli Martion kirjasta Vektorianalyysi (saatavilla avoimesti Helsingin Yliopiston Helda-palvelusta). Dokumentin tarkoitus on parantaa sekä korjata Martion kirjassa ilmenevät virheet että lisätä puuttuvia määritelmiä, jotta kokonaisuus olisi tarpeeksi täsmällinen että sen voisi formalisoida. Dokumentin sekaan on kirjoitettu Sauli Lindbergin Vektorianalyysi II kurssin luentomonisteesta hyödyllisiä tuloksia.

Dokumentti on tehty Leanblueprint-työkalulla, joka mahdollistaa isojen formalisointiprojektien koordinoinnin. Dokumentin tarkoitus ei tällä hetkellä ole kuitenkaan formalisoida Martion kirjan tuloksia Lean-todistusassistentilla.

Dokumentin verkkoversion vasemmasta reunasta löytyy Dependency graph joka vie interaktiiviseen verkkomuotoiseen esitykseen dokumentin määritelmistä ja lauseista.

Lisäksi jokaisen kappaleena alta löytyy muuttujia jotka otetaan kyseisen kappaleen loppuun asti universaalisti kvantifioituna.