Theorem Relation.onFun_map_eq_of_injective

Modification history

2026-09-10 16:50
Mathlib/Logic/Relation.lean
feat(Logic/Relation): `Map r f g ≤ s ↔ r ≤ s.bicompl f g` (#38432) …
Modified Relation.onFun_map_eq_of_injectiveView on Github →
2025-12-01 11:03
Mathlib/Logic/Relation.lean
feat(Logic/Relation): lemmas relating `Relation.Map` and `Function.onFun` (#30416)
Added Relation.onFun_map_eq_of_injectiveView on Github →