Commit 2021-03-06 21:16 b280b005
View on Github →feat(data/set/basic): add set.set_ite
(#6557)
I'm going to use it as source
and target
in
local_equiv.piecewise
and local_homeomorph.piecewise
. There are
many non-defeq ways to define this set and I think that it's better to
have a name than to ensure that we always use the same formula.