Theorem Relation.map_onFun_le

Modification history

2026-07-01 01:31

Mathlib/Logic/Relation.lean

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

Modified Relation.map_onFun_le 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.map_onFun_le View on Github →