Commits · Subset · Micaela Mayero / Numerical Analysis in Coq

Feb 08, 2024
- Borrow patches from master branch. · 4ec19a10
  François Clément authored 1 year ago
  
  4ec19a10
Feb 06, 2024
- WIP: Coq-8.16 compat + merge with master. · 58dca76c
  François Clément authored 1 year ago
  
  58dca76c
- WIP: Coq-8.16 compatibility + pre-merge with master branch. · 18f4fe8a
  François Clément authored 1 year ago
```
It is not fully compiling yet!
```
  18f4fe8a
- Borrow everything from master branch! · ac99d88f
  François Clément authored 1 year ago
```
Now this is compiling with Coq-8.16.
```
  ac99d88f
Jul 08, 2022
- WIP: proof of Basisf_Prod. · d8450ecc
  François Clément authored 2 years ago
  
  d8450ecc
- Use new API: Open_Inter_finite -> Open_Inter. · 336b65b7
  François Clément authored 2 years ago
  
  336b65b7
- Open: Inter_finite -> Inter. · 5144ddc9
  François Clément authored 2 years ago
  
  5144ddc9
Jul 01, 2022
- Add alternative result. · 3a81b48e
  François Clément authored 2 years ago
  
  3a81b48e
- Mv. · 268f865e
  François Clément authored 2 years ago
  
  268f865e
- Add alternative result. · 9002960c
  François Clément authored 2 years ago
  
  9002960c
- Renaming + cleaning (of doubles and useless results). · 44897cb9
  François Clément authored 2 years ago
```
Mv def of continuity (to Set_system_def_any).
```
  44897cb9
- Propagate new API (Subset). · 115b9ac9
  François Clément authored 2 years ago
```
Simplify proof of all_is_Basisf.
```
  115b9ac9
- Use new API (Subset). · 9be0a127
  François Clément authored 2 years ago
```
Mv def of continuity.
```
  9be0a127
- Add results about Subset (when A = emptyset or fullset). · 414b0c66
  François Clément authored 2 years ago
  
  414b0c66
- Make P an explicit argument. · e6e1b2d6
  François Clément authored 2 years ago
  
  e6e1b2d6
- Proof of Open_equiv. · 0a214db9
  François Clément authored 2 years ago
```
Some cleaning.
```
  0a214db9
- Add results about {Inter,Union}_finite_closure_wF. · eefc3a94
  François Clément authored 2 years ago
  
  eefc3a94
- Unify results about {Inter,Union}*_closure. · e95988a4
  François Clément authored 2 years ago
  
  e95988a4
- Add {Inter,Union}f_finite and Union_finite_closure_wE. · da07e9a7
  François Clément authored 2 years ago
  
  da07e9a7
- Add results on double {inter,union}_seq. · c4bc91c7
  François Clément authored 2 years ago
  
  c4bc91c7
- Unify naming. · e1273b77
  François Clément authored 2 years ago
  
  e1273b77
- WIP: unify naming and results about {Inter,Union}*_closure. · 03b21c85
  François Clément authored 2 years ago
  
  03b21c85
Jun 30, 2022
- Proof of Uac_Ifc_wF_is_Open. · 8de12aed
  François Clément authored 2 years ago
```
WIP: Open_equiv.
```
  8de12aed
- Propagate new API. · 8e9d617f
  François Clément authored 2 years ago
  
  8e9d617f
- Unify: renaming + change order of equivalence. · 80f2211b
  François Clément authored 2 years ago
  
  80f2211b
- WIP: add finite type int_0. · 893d4bdd
  François Clément authored 2 years ago
  
  893d4bdd
- Add monotony of {Inter,Union}_any_closure. · a9f5e7df
  François Clément authored 2 years ago
  
  a9f5e7df
- Propagate new API (Inter_with_empty -> Inter_wEmpty). · 277490ed
  François Clément authored 2 years ago
  
  277490ed
- Propagate new API (Inter_finite_closure and Inter_finite_closure_wF). · c1777b85
  François Clément authored 2 years ago
  
  c1777b85
- Renaming (Inter_with_empty -> Inter_wEmpty). · de7dd977
  François Clément authored 2 years ago
```
Add results about Inter and Union when adding {empty,full}set.
```
  de7dd977
- Split both aspects. · c86706a3
  François Clément authored 2 years ago
  
  c86706a3
Jun 29, 2022
- WIP: trying new API (Inter_finite_closure with fullset). · 65154e21
  François Clément authored 2 years ago
  
  65154e21
- Propagate new API (Inter_finite_closure now includes fullset). · 9931a69d
  François Clément authored 2 years ago
  
  9931a69d
- Add fullset (as nullary intersection). · aa63d89e
  François Clément authored 2 years ago
  
  aa63d89e
- WIP: Uac_Ifc_is_Open + Open_equiv. · 7613d4ee
  François Clément authored 2 years ago
  
  7613d4ee
- Propagate new API (renaming). · 6508f761
  François Clément authored 2 years ago
  
  6508f761
- Unify results about {empty,full}{,set}. · 1806feff
  François Clément authored 2 years ago
  
  1806feff
- WIP: interf_any_interp_any_comm. · 28fbec83
  François Clément authored 2 years ago
  
  28fbec83
- Hide admit (it is in comment). · 3d308f6c
  François Clément authored 2 years ago
  
  3d308f6c
- Propagate renaming. · 64913ae0
  François Clément authored 2 years ago
  
  64913ae0