Mathlib v3 is deprecated. Go to Mathlib v4

Theorem relation.refl_gen.mono

Modification history

2022-01-27 23:05
src/logic/relation.lean
feat(order/succ_pred/relation): `succ`/`pred` inductions on relations (#11518) …
Added relation.refl_gen.monoView on Github →