Commits · Tonelli.1.0 · Micaela Mayero / Numerical Analysis in Coq

Feb 07, 2022
- Remove spurious whites. · 751198b1
  François Clément authored 3 years ago
  
  751198b1
- Comment all admitted stuff (dmit -> glop). · b9b1ce78
  François Clément authored 3 years ago
  
  b9b1ce78
Jan 29, 2022
- Renaming. · 0804fa1a
  François Clément authored 3 years ago
  
  _ge_0 _empty -> _nonneg _False -> _emptyset Use emptyset and nonneg.
  0804fa1a
- Add results on singletons. · c5ddacf2
  François Clément authored 3 years ago
  
  Proofs of diffuseness.
  c5ddacf2
Jan 27, 2022
- WIP: add props of Lebesgue measure. · 25c3c5cc
  François Clément authored 3 years ago
  
  25c3c5cc
Jan 18, 2022
- Naming: *non_neg* -> *nonneg*. · b462d2ba
  François Clément authored 3 years ago
  
  b462d2ba
- Unify naming: remove most prime from statement names (-> _alt, _rev, _aux). · 53cf56d8
  François Clément authored 3 years ago
  
  *_seq'* -> *_seq_Rbar*
  53cf56d8
Dec 17, 2021
- dmit -> glop. · b3ee6487
  François Clément authored 3 years ago
  
  Comment lemmas using not yet proved results.
  b3ee6487
Dec 08, 2021
- Some cleaning + hide (= comment out) admitted stuff. · d3b50977
  François Clément authored 3 years ago
  
  d3b50977
Oct 28, 2021
- Revert "Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysis" · bf09a470
  François Clément authored 3 years ago
  
  This reverts commit ab8689c9, reversing changes made to eb9897ee.
  bf09a470
Oct 26, 2021
- sigma_algebra_R_Rbar.v -> sigma_algebra_R_Rbar-old.v · 4c03ae3e
  François Clément authored 3 years ago
  
  sigma_algebra_R_Rbar_new.v -> sigma_algebra_R_Rbar.v
  4c03ae3e
Sep 07, 2021
- initial sept. 2021 · fb0ef3a3
  Micaela Mayero authored 3 years ago
  
  fb0ef3a3