`IndisputableMonolith.Relativity.Analysis`

IndisputableMonolith/Relativity/Analysis.lean · 12 lines · 0 declarations

Explainer status: pending

   1-- Analysis Module Aggregator
   2import IndisputableMonolith.Relativity.Analysis.Landau
   3import IndisputableMonolith.Relativity.Analysis.Limits
   4
   5/-!
   6# Analysis Module
   7
   8Mathematical analysis utilities:
   9- `Landau` - Landau big-O notation for error bounds
  10- `Limits` - Limit theorems and continuity
  11-/
  12

source mirrored from github.com/jonwashburn/shape-of-logic