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)
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)