Theorems · Theorem · logic and foundations

Set.piecewise_compl

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

Defined in

Mathlib.Data.Set.Piecewise

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidableDecidable