Mathlib v3 is deprecated. Go to Mathlib v4

Def embedding

Modification history

2019-07-09 20:34

src/topology/maps.lean

refactor(topology/*): define and use dense_inducing (#1193) …

Deleted embedding View on Github →

2019-03-03 19:05

src/topology/constructions.lean

chore(topology): Splits topology.basic and topology.continuity (#785) …

Modified embedding View on Github →

2017-08-10 16:36

topology/continuity.lean

construct reals as complete, linear ordered field

Added embedding View on Github →