Mathlib v3 is deprecated. Go to Mathlib v4

Def galois_insertion.monotone_intro

Modification history

2019-11-18 20:32
src/order/galois_connection.lean
feat(data/real/nnreal): define `nnreal.gi : galois_insertion of_real coe` (#1699)
Added galois_insertion.monotone_introView on Github →