Mathlib v3 is deprecated. Go to Mathlib v4

Theorem embedding_open

Modification history

2021-02-22 14:12

src/topology/maps.lean

refactor(order/filter,topology): review API (#6347) …

Deleted embedding_open View on Github →

2019-03-03 19:05

src/topology/constructions.lean

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

Modified embedding_open View on Github →

2017-08-10 16:36

topology/continuity.lean

construct reals as complete, linear ordered field

Added embedding_open View on Github →