mathlib3
b338240e - feat(topology/constructions): a finite product of discrete spaces is discrete (#6088)

Commit

4 years ago

feat(topology/constructions): a finite product of discrete spaces is discrete (#6088) From `lean-liquid`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents

e4369fe3

mathlib3 b338240e - feat(topology/constructions): a finite product of discrete spaces is discrete (#6088)

mathlib3
b338240e - feat(topology/constructions): a finite product of discrete spaces is discrete (#6088)