Theorem Relation.le_onFun_map

Modification history

2026-07-01 01:31

Mathlib/Logic/Relation.lean

chore(Logic/Relation): use `≤` to spell subrelation (#30526) …

Modified Relation.le_onFun_map View on Github →

2025-12-01 11:03

Mathlib/Logic/Relation.lean

feat(Logic/Relation): lemmas relating `Relation.Map` and `Function.onFun` (#30416)

Added Relation.le_onFun_map View on Github →