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

fix error

Browse source
This commit is contained in:
Floris van Doorn 2017-06-06 12:00:08 -04:00
parent 56f7ea093e
commit dc2c697885
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
homotopy/spectrum.hlean
View file

@ -40,7 +40,7 @@ abbreviation prespectrum := gen_prespectrum +ℤ
definition prespectrum.mk (Y : ℤ → Type*) (e : Π(n : ℤ), Y n →* Ω (Y (n+1))) : prespectrum :=
gen_prespectrum.mk Y e
abbreviation spectrum := gen_spectrum +ℤ
abbreviation spectrum.mk (Y : ℤ → Type*) (e : Π(n : ℤ), Y n ≃* Ω (Y (n+1))) : prespectrum :=
abbreviation spectrum.mk (Y : prespectrum) (e : is_spectrum Y) : spectrum :=
gen_spectrum.mk Y e
namespace spectrum
@ -108,7 +108,7 @@ namespace spectrum
end
protected definition of_gen_indexed [constructor] {N : succ_str} (z : N) (E : gen_spectrum N) : spectrum :=
spectrum.mk (psp_of_gen_indexed z E) (is_spectrum_of_gen_indexed z E)
gen_spectrum.mk (psp_of_gen_indexed z E) (is_spectrum_of_gen_indexed z E)
-- Generally it's easiest to define a spectrum by giving 'equiv's
-- directly. This works for any indexing succ_str.