Commits · e9998154815c7781dcdef84289e37fae94c38162 · Micaela Mayero / Numerical Analysis in Coq

Mar 17, 2022
- Unify with Lebesgue folder: CoqMakefile -> Makefile. · e9998154
  François Clément authored 3 years ago
  
  e9998154
- Proofs of image_diff, image_compl and preimage_empty_equiv. · b0a05d81
  François Clément authored 3 years ago
  
  b0a05d81
- Proofs of image_{union,inter}*. · cd311819
  François Clément authored 3 years ago
  
  cd311819
Mar 16, 2022
- Add Image/Preimage. · 6b466dc7
  François Clément authored 3 years ago
  
  WIP: add facts about Image/Preimage.
  6b466dc7
- Add measurable_Rbar_gen_lub_up_{m,p}. · 42f1fbda
  François Clément authored 3 years ago
  
  42f1fbda
- Equiv -> impl. · dc3b0de3
  François Clément authored 3 years ago
  
  dc3b0de3
- Add image/preimage. · 71731d6c
  François Clément authored 3 years ago
  
  WIP: many facts about image/preimage.
  71731d6c
Mar 11, 2022
- WIP: proofs of measurable_Borel_Rbar_eq_(l|g)(t|e). · 4abd489e
  François Clément authored 3 years ago
  
  Proofs of measurable_Rbar_*.
  4abd489e
- Order (imports) + renaming (section). · 730777b8
  François Clément authored 3 years ago
  
  730777b8
- Add Rbar_oo_diag_is_empty. · cefb2c05
  François Clément authored 3 years ago
  
  Remove useless.
  cefb2c05
Mar 10, 2022
- Proof of measurable_Rbar_R_correct and measurable_R_Rbar_correct. · 11d85fc4
  François Clément authored 3 years ago
  
  11d85fc4
- WIP: reorganize proof of measurable_Rbar_R_correct. · d66548c0
  François Clément authored 3 years ago
  
  Renaming: measurable_Rbar_Borel -> measurable_Rbar_R measurable_Rbar_Borel_alt -> measurable_R_Rbar.
  d66548c0
- Symmetrical proof. · cbfffdc2
  François Clément authored 3 years ago
  
  cbfffdc2
- Add symmetrical result. · b8481bcb
  François Clément authored 3 years ago
  
  b8481bcb
- Factor proof. · 021d5420
  François Clément authored 3 years ago
  
  021d5420
- Add Rbar_second_countable. · 8d590f01
  François Clément authored 3 years ago
  
  8d590f01
- Useless. · fc7a1d32
  François Clément authored 3 years ago
  
  fc7a1d32
- Add Even_Odd_dec (since Even is obsolete). · 7ad9f3bd
  François Clément authored 3 years ago
  
  7ad9f3bd
Mar 09, 2022
- WIP: proof of measurable_Rbar_Borel_correct. · 004425ff
  François Clément authored 3 years ago
  
  004425ff
- Coquelicot -> Hierarchy. · 962e89ba
  François Clément authored 3 years ago
  
  962e89ba
- Suppress dependency wrt Coquelicot. · 8a4e7b64
  François Clément authored 3 years ago
  
  8a4e7b64
Mar 08, 2022
- rewrite -> apply. · b294d0a3
  François Clément authored 3 years ago
  
  b294d0a3
- Proof of measurable_Borel_prod_eq. · 34fd7ad1
  François Clément authored 3 years ago
  
  34fd7ad1
- New API. · 6f2f8cf1
  François Clément authored 3 years ago
  
  6f2f8cf1
- Use new abstract formalization of topological bases. · f3fdb3df
  François Clément authored 3 years ago
  
  f3fdb3df
- Add open_prod, and section on topological basis. · 4a82d181
  François Clément authored 3 years ago
  
  4a82d181
Mar 06, 2022
- WIP: measurable_Borel_prod_eq. · 78bac00b
  François Clément authored 3 years ago
  
  78bac00b
Mar 04, 2022
- Remove useless. · f1cbb62e
  François Clément authored 3 years ago
  
  f1cbb62e
Mar 03, 2022
- WIP: measurable_R2_eq_Borel. · ce3a8396
  François Clément authored 3 years ago
  
  ce3a8396
- Cleaning + alternatives to try? · 419df51d
  François Clément authored 3 years ago
  
  419df51d
- Fill missing proofs: mainly Rbar_interval_eq, and Rbar_subset_open_correct. · 63586bbf
  François Clément authored 3 years ago
  
  63586bbf
- Unify naming: R_is_open -> R_subset_open. · 0d8973a3
  François Clément authored 3 years ago
  
  0d8973a3
- Add Rbar_glb_lt_ex and Rbar_lub_gt_ex. · f956a547
  François Clément authored 3 years ago
  
  f956a547
- Cleaning already commented old stuff. · 0672f20e
  François Clément authored 3 years ago
  
  0672f20e
- Make it compile. · 12990487
  François Clément authored 3 years ago
  
  12990487
- New formalization + doc. · e63f1bea
  François Clément authored 3 years ago
  
  Proof of Rbar_ray_eq.
  e63f1bea
- Simpler? · 6b4d5116
  François Clément authored 3 years ago
  
  6b4d5116
Mar 02, 2022
- Change order. · 6d526ac3
  François Clément authored 3 years ago
  
  6d526ac3
- Add Rbar_le_equiv. · aee038e4
  François Clément authored 3 years ago
  
  aee038e4
- Merge · 9649cc18
  Sylvie Boldo authored 3 years ago
  
  Merge branch 'master' of https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis
  9649cc18