Commit 2023-01-30 09:21 2f3db46e

View on Github →

Feat: add new Set.univ_pi_piecewise, rename the old lemma to Set.univ_pi_piecewise_univ (#1904)

Estimated changes

Modified Mathlib/Data/Set/Function.lean

modified theorem Set.univ_pi_piecewise

added theorem Set.univ_pi_piecewise_univ

Modified Mathlib/Order/Filter/Pi.lean