Theorems · Theorem · logic and foundations

Set.piecewise_eq_of_mem

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

Defined in

Mathlib.Data.Set.Piecewise

Cited by

49 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

Decidable