Commit 2026-02-09 12:02 f1fb168d

View on Github →

feat: lemmas for Set.range fun x : {a, b, ...} ↦ ... (#34639) These allow simp to simplify e.g. Set.range f for f : {a, b, c} → β to {f a, f b, f c}. Used in the CGT repo.

Estimated changes

Modified Mathlib/Data/Set/Image.lean

added theorem Set.range_insert

added theorem Set.range_singleton

modified theorem Set.range_unique