Theorem SetRel.image_sUnion

Modification history

2026-09-08 19:42

Mathlib/Basic/Rel.lean

perf(Basic/Rel): use `grind` instead of `aesop` (#42405) …

Modified SetRel.image_sUnion View on Github →

2025-12-15 18:48

Mathlib/Data/Rel.lean

feat: `SetRel.(pre)image` of `iUnion` and `sUnion` (#32847)

Added SetRel.image_sUnion View on Github →