michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix the statement of susp_product.

Browse source
This commit is contained in:
favonia 2017-06-07 09:38:33 -06:00
parent c19c885de3
commit df3ce3872f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
susp_product.hlean
View file

@ -1,5 +1,5 @@
import core
open susp smash pointed wedge prod
definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ (X ∧ Y)) :=
definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ ⅀ (X ∧ Y)) :=
sorry