Commits · 0a214db971c1235cbe8927c6367d5dd42b7ee935 · Micaela Mayero / Numerical Analysis in Coq · GitLab

Snippets Groups Projects

Jul 01, 2022
- 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
- Propagate renaming. · a097caa6
  François Clément authored 2 years ago
  
  a097caa6
- Add results about {Inter,Union}_finite_closure. · 448d4d5e
  François Clément authored 2 years ago
```
Some renaming.
```
  448d4d5e
- Add append_in. · abda7ead
  François Clément authored 2 years ago
  
  abda7ead
- WIP: new proof path. · 9ae1a23a
  François Clément authored 2 years ago
  
  9ae1a23a
Jun 28, 2022
- WIP: Inter_finite_closure_is_Basisp. · 2989eae3
  François Clément authored 2 years ago
  
  2989eae3
- Use new API. · c65c3b5b
  François Clément authored 2 years ago
  
  c65c3b5b
- WIP: Inter_finite_closure_is_Basisp. · b7ce666a
  François Clément authored 2 years ago
  
  b7ce666a
- Add results linking {inter,union}_finite and {inter,union}f_any. · 57ef2c8f
  François Clément authored 2 years ago
  
  57ef2c8f
- Renaming. · b8562fe0
  François Clément authored 2 years ago
  
  b8562fe0
- Rm now useless hypotheses. · 1f9f7434
  François Clément authored 2 years ago
  
  1f9f7434
- Mv stuff + use explicit arguments to get generality inside sections. · e882fe49
  François Clément authored 2 years ago
  
  e882fe49
- Proof of Inter_any_closure_complp_any_eq. · 86842ab5
  François Clément authored 2 years ago
```
Add Union_any_closure_complp_any_eq.
```
  86842ab5
- Renaming: incl_complp_any_equiv -> inclp_any_complp_any_equiv. · f1fe03cd
  François Clément authored 2 years ago
  
  f1fe03cd
- Renaming: complp_any_equiv -> complp_any_eq. · 32f850c8
  François Clément authored 2 years ago
```
Add incl_complp_any_equiv_alt.
```
  32f850c8
- Add results about {Inter,Union}_any. · acaad1b6
  François Clément authored 2 years ago
  
  acaad1b6