Mathlib v3 is deprecated. Go to Mathlib v4

Def set.piecewise

Modification history

2021-03-23 15:29

src/logic/function/basic.lean

lint(*): split long lines (#6833)

Modified set.piecewise View on Github →

2020-01-26 15:54

src/logic/function.lean

feat(linear_algebra/multilinear): image of sum (#1908) …

Added set.piecewise View on Github →