Theorems · Definition

Set.piecewise

{α : Type u} →
  {β : α → Sort v} → (s : Set α) → ((i : α) → β i) → ((i : α) → β i) → [(j : α) → Decidable (j ∈ s)] → (i : α) → β i

s.piecewise f g is the function equal to f on the set s, and to g on its complement.

Defined in

Mathlib.Logic.Function.Basic

Cited by

136 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 12 definitions · uses no axioms

Assumes

Decidable