Mathlib v3 is deprecated. Go to Mathlib v4

Def function.embedding.option_map

Modification history

2022-05-27 02:02
src/logic/embedding.lean
feat(order/bounded_order): define `with_bot.map` and `with_top.map` (#14163) …
Added function.embedding.option_mapView on Github →