Commit 2025-01-10 13:20 804cb796

View on Github →

feat: If s ∆ t is finite, then s ∆ u is finite iff t ∆ u is (#20574) Also make Set.Finite.diff have one less explicit argument. From my PhD (LeanCamCombi)

Estimated changes