Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-20 11:16 15a6af22

View on Github →

feat(topology/opens): continuous.comap : opens Y → opens X (#1061)

feat(topology/opens): continuous.comap : opens Y → opens X From the perfectoid project.
Update opens.lean

Estimated changes

Modified src/topology/opens.lean

added def continuous.comap

added theorem continuous.comap_id

added theorem continuous.comap_mono