Piecewise functions #
This file contains basic results on piecewise defined functions.
@[deprecated Set.piecewise_eq_of_notMem (since := "2025-05-23")]
theorem
Set.piecewise_eq_of_not_mem
{α : Type u_1}
{δ : α → Sort u_7}
(s : Set α)
(f g : (i : α) → δ i)
[(j : α) → Decidable (j ∈ s)]
{i : α}
(hi : i ∉ s)
:
Alias of Set.piecewise_eq_of_notMem
.
theorem
Set.piecewise_singleton
{α : Type u_1}
{β : Type u_2}
(x : α)
[(y : α) → Decidable (y ∈ {x})]
[DecidableEq α]
(f g : α → β)
: