Commit 2022-10-15 19:03 5ea225ec

View on Github →

feat(data/set/function): add set.eq_on_union (#16984) Also add set.eq_on.union and turn set.comp_eq_of_eq_on_range into an iff lemma set.eq_on_range.

Estimated changes

Modified src/data/set/function.lean

deleted theorem set.comp_eq_of_eq_on_range

added theorem set.eq_on.union

added theorem set.eq_on_range

added theorem set.eq_on_union