Commits · 64913ae084506f7f364bab4b12969191b1e33408 · Micaela Mayero / Numerical Analysis in Coq

Jun 29, 2022
- 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
- WIP: De Morgan's laws for {Inter,Union}_any_closure. · d3ad6e15
  François Clément authored 2 years ago
  
  d3ad6e15
- Doc. · 950b9c2f
  François Clément authored 2 years ago
  
  950b9c2f
- Fix proof of {Inter,Union}_any_closure_is_Open. · ed736656
  François Clément authored 2 years ago
  
  ed736656
- Renaming (and modif statement): · 869eaee5
  François Clément authored 2 years ago
```
Unionf_any_Interf_any_complp_any -> Interf_any_complp_any_equiv
Interf_any_Unionf_any_complp_any -> Unionf_any_complp_any_equiv
Unionf_any_Interf_any_equiv -> Interf_any_Unionf_any_equiv
```
  869eaee5
- Fix statement and proof of Inter_any_closure_Union. · 2c55a2a8
  François Clément authored 2 years ago
  
  2c55a2a8
Jun 27, 2022
- Mv + fix proof of Union_any_closure_Inter. · 79c7a006
  François Clément authored 2 years ago
  
  79c7a006
- Add results about x_interp_map_any. · df73a0b3
  François Clément authored 2 years ago
  
  df73a0b3
Jun 24, 2022
- Mv upward. · 42647a40
  François Clément authored 2 years ago
  
  42647a40
- WIP... · fd4d0ec9
  François Clément authored 2 years ago
  
  fd4d0ec9
Jun 23, 2022
- WIP. · 3a58aecf
  François Clément authored 2 years ago
  
  3a58aecf
- Add results about {Inter,Union}_any_closure. · 57aab806
  François Clément authored 2 years ago
  
  57aab806
- Rm unionp_any_emptyset (= unionp_any_nullary). · f9896912
  François Clément authored 2 years ago
  
  f9896912
- WIP: is_Open_Union_any_closure. · f799a924
  François Clément authored 2 years ago
  
  f799a924
- Add results about Union_any_closure. · 4713009a
  François Clément authored 2 years ago
  
  4713009a
- Add unionp_any_emptyset. · 013cb1ab
  François Clément authored 2 years ago
  
  013cb1ab
- Use new generic results from Set_system_any.v. · 3a17b60d
  François Clément authored 2 years ago
  
  3a17b60d
- Use new result Union_any_inter_equiv. · ab61ec0e
  François Clément authored 2 years ago
```
WIP: add is_Open_Union_any_closure.
```
  ab61ec0e
- Add Union_any_inter_equiv. · 58e56e3b
  François Clément authored 2 years ago
  
  58e56e3b
- Mv "any" stuff to _any file. · df7c6465
  François Clément authored 2 years ago
  
  df7c6465
- Line too long. · 23eb357f
  François Clément authored 2 years ago
  
  23eb357f
- Use new API (interP_{l,r}). · 32004640
  François Clément authored 2 years ago
  
  32004640
- Add interP_{l,r}. · e8bca60f
  François Clément authored 2 years ago
  
  e8bca60f
Jun 22, 2022
- Prove and split result into is_Basisp_full and is_Basisp_inter. · 4c47404b
  François Clément authored 2 years ago
  
  4c47404b
- Unify style. · 93898702
  François Clément authored 2 years ago
  
  93898702