Theorems · Theorem · order theory

Finset.compl_filter

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : α → Prop) [inst_2 : DecidablePred p]
  [inst_3 : (x : α) → Decidable ¬p x], (Finset.filter p Finset.univ)ᶜ = {x | ¬p x}

Defined in

Mathlib.Data.Finset.BooleanAlgebra

Cited by

11 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqDecidablePredDecidable