Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_sigma_mk

Modification history

2019-05-13 23:54

src/topology/constructions.lean

feat(topology/constructions): topology of sum types (#1016)

Added continuous_sigma_mk View on Github →