Theorems · Theorem · logic and foundations

Set.apply_piecewise

∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
  {δ' : α → Sort u_8} (h : (i : α) → δ i → δ' i) {x : α},
  h x (s.piecewise f g x) = s.piecewise (fun x => h x (f x)) (fun x => h x (g x)) x

Defined in

Mathlib.Data.Set.Piecewise

Cited by

3 results in Mathlib

Foundations

Depth 8 from the axioms · uses propext

Assumes

Decidable