Theorems · Theorem · logic and foundations

Set.piecewise_op

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

Defined in

Mathlib.Data.Set.Piecewise

Cited by

4 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext, Quot.sound

Assumes

Decidable