Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-10 00:40 f1683a9e

View on Github →

feat(data/set/basic): inclusion map (#906)

feat(data/set/basic): inclusion map
add continuous_inclusion
minor style change

Estimated changes

Modified src/data/set/basic.lean

added def set.inclusion

added theorem set.inclusion_inclusion

added theorem set.inclusion_injective

added theorem set.inclusion_self

Modified src/topology/constructions.lean

added theorem continuous_inclusion