Commit 2025-12-01 11:03 5ea74736

View on Github →

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

Estimated changes

Modified Mathlib/Logic/Relation.lean

added theorem Relation.le_onFun_map

added theorem Relation.map_onFun_eq_of_surjective

added theorem Relation.map_onFun_le

added theorem Relation.map_onFun_map_eq_map

added theorem Relation.onFun_map_eq_of_injective

added theorem Relation.onFun_map_onFun_eq_onFun

added theorem Relation.onFun_map_onFun_iff_onFun