Documentation

Mathlib.Data.Finset.BooleanAlgebra

Finsets are a boolean algebra #

This file provides the BooleanAlgebra (Finset α) instance, under the assumption that α is a Fintype.

Main results #

source
theorem Finset.Nonempty.eq_univ {α : Type u_1} {s : Finset α} [Fintype α] [Subsingleton α] :
s.Nonempty → s = univ
source
theorem Finset.univ_nonempty_iff {α : Type u_1} [Fintype α] :
univ.Nonempty ↔ Nonempty α
source
@[simp]
theorem Finset.univ_nonempty {α : Type u_1} [Fintype α] [Nonempty α] :
univ.Nonempty
source
theorem Finset.univ_eq_empty_iff {α : Type u_1} [Fintype α] :
univ = ∅ ↔ IsEmpty α
source
theorem Finset.univ_nontrivial_iff {α : Type u_1} [Fintype α] :
univ.Nontrivial ↔ Nontrivial α
source
theorem Finset.univ_nontrivial {α : Type u_1} [Fintype α] [h : Nontrivial α] :
univ.Nontrivial
source
@[simp]
theorem Finset.univ_eq_empty {α : Type u_1} [Fintype α] [IsEmpty α] :
univ = ∅
source
@[simp]
theorem Finset.univ_unique {α : Type u_1} [Fintype α] [Unique α] :
univ = {default}
source
instance Finset.boundedOrder {α : Type u_1} [Fintype α] :
BoundedOrder (Finset α)
Equations
    source
    @[simp]
    theorem Finset.top_eq_univ {α : Type u_1} [Fintype α] :
    ⊤ = univ
    source
    theorem Finset.ssubset_univ_iff {α : Type u_1} [Fintype α] {s : Finset α} :
    s ⊂ univ ↔ s ≠ univ
    source
    @[simp]
    theorem Finset.univ_subset_iff {α : Type u_1} [Fintype α] {s : Finset α} :
    univ ⊆ s ↔ s = univ
    source
    theorem Finset.codisjoint_left {α : Type u_1} {s t : Finset α} [Fintype α] :
    Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t
    source
    theorem Finset.codisjoint_right {α : Type u_1} {s t : Finset α} [Fintype α] :
    Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∈ s
    source
    instance Finset.booleanAlgebra {α : Type u_1} [Fintype α] [DecidableEq α] :
    BooleanAlgebra (Finset α)
    Equations
      source
      theorem Finset.sdiff_eq_inter_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s t : Finset α) :
      s \ t = s ∩ tᶜ
      source
      theorem Finset.compl_eq_univ_sdiff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      sᶜ = univ \ s
      source
      @[simp]
      theorem Finset.mem_compl {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} :
      a ∈ sᶜ ↔ a ∉ s
      source
      theorem Finset.notMem_compl {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} :
      a ∉ sᶜ ↔ a ∈ s
      source
      @[deprecated Finset.notMem_compl (since := "2025-05-23")]
      theorem Finset.not_mem_compl {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} :
      a ∉ sᶜ ↔ a ∈ s

      Alias of Finset.notMem_compl.

      source
      @[simp]
      theorem Finset.coe_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      ↑sᶜ = (↑s)ᶜ
      source
      @[simp]
      theorem Finset.compl_subset_compl {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
      sᶜ ⊆ tᶜ ↔ t ⊆ s
      source
      @[simp]
      theorem Finset.compl_ssubset_compl {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
      sᶜ ⊂ tᶜ ↔ t ⊂ s
      source
      theorem Finset.subset_compl_comm {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
      s ⊆ tᶜ ↔ t ⊆ sᶜ
      source
      @[simp]
      theorem Finset.subset_compl_singleton {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} :
      s ⊆ {a}ᶜ ↔ a ∉ s
      source
      @[simp]
      theorem Finset.compl_empty {α : Type u_1} [Fintype α] [DecidableEq α] :
      ∅ᶜ = univ
      source
      @[simp]
      theorem Finset.compl_univ {α : Type u_1} [Fintype α] [DecidableEq α] :
      univᶜ = ∅
      source
      @[simp]
      theorem Finset.compl_eq_empty_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      sᶜ = ∅ ↔ s = univ
      source
      @[simp]
      theorem Finset.compl_eq_univ_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      sᶜ = univ ↔ s = ∅
      source
      @[simp]
      theorem Finset.union_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      s ∪ sᶜ = univ
      source
      @[simp]
      theorem Finset.inter_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      s ∩ sᶜ = ∅
      source
      @[simp]
      theorem Finset.compl_union {α : Type u_1} [Fintype α] [DecidableEq α] (s t : Finset α) :
      (s ∪ t)ᶜ = sᶜ ∩ tᶜ
      source
      @[simp]
      theorem Finset.compl_inter {α : Type u_1} [Fintype α] [DecidableEq α] (s t : Finset α) :
      (s ∩ t)ᶜ = sᶜ ∪ tᶜ
      source
      @[simp]
      theorem Finset.compl_erase {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} :
      (s.erase a)ᶜ = insert a sᶜ
      source
      @[simp]
      theorem Finset.compl_insert {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} :
      (insert a s)ᶜ = sᶜ.erase a
      source
      theorem Finset.insert_compl_insert {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} (ha : a ∉ s) :
      insert a (insert a s)ᶜ = sᶜ
      source
      @[simp]
      theorem Finset.insert_compl_self {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) :
      insert x {x}ᶜ = univ
      source
      @[simp]
      theorem Finset.compl_filter {α : Type u_1} [Fintype α] [DecidableEq α] (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] :
      (filter p univ)ᶜ = {x : α | ¬p x}
      source
      theorem Finset.compl_ne_univ_iff_nonempty {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      sᶜ ≠ univ ↔ s.Nonempty
      source
      theorem Finset.compl_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (a : α) :
      {a}ᶜ = univ.erase a
      source
      theorem Finset.insert_inj_on' {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      Set.InjOn (fun (a : α) => insert a s) ↑sᶜ
      source
      theorem Finset.image_univ_of_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] {f : β → α} (hf : Function.Surjective f) :
      image f univ = univ
      source
      @[simp]
      theorem Finset.image_univ_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] (f : β ≃ α) :
      image (⇑f) univ = univ
      source
      @[simp]
      theorem Finset.univ_inter {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      univ ∩ s = s
      source
      @[simp]
      theorem Finset.inter_univ {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      s ∩ univ = s
      source
      @[simp]
      theorem Finset.inter_eq_univ {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
      s ∩ t = univ ↔ s = univ ∧ t = univ
      source
      theorem Finset.singleton_eq_univ {α : Type u_1} [Fintype α] [Subsingleton α] (a : α) :
      {a} = univ
      source
      theorem Finset.map_univ_of_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : β ↪ α} (hf : Function.Surjective ⇑f) :
      map f univ = univ
      source
      @[simp]
      theorem Finset.map_univ_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : β ≃ α) :
      map f.toEmbedding univ = univ
      source
      theorem Finset.univ_map_equiv_to_embedding {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (e : α ≃ β) :
      map e.toEmbedding univ = univ
      source
      @[simp]
      theorem Finset.univ_filter_exists {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) [Fintype β] [DecidablePred fun (y : β) => ∃ (x : α), f x = y] [DecidableEq β] :
      {y : β | ∃ (x : α), f x = y} = image f univ
      source
      theorem Finset.univ_filter_mem_range {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) [Fintype β] [DecidablePred fun (y : β) => y ∈ Set.range f] [DecidableEq β] :
      {y : β | y ∈ Set.range f} = image f univ

      Note this is a special case of (Finset.image_preimage f univ _).symm.

      source
      theorem Finset.coe_filter_univ {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] :
      ↑(filter p univ) = {x : α | p x}
      source
      @[simp]
      theorem Finset.subtype_eq_univ {α : Type u_1} {s : Finset α} {p : α → Prop} [DecidablePred p] [Fintype { a : α // p a }] :
      Finset.subtype p s = univ ↔ ∀ ⦃a : α⦄, p a → a ∈ s
      source
      @[simp]
      theorem Finset.subtype_univ {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a : α // p a }] :
      Finset.subtype p univ = univ
      source
      theorem Finset.univ_map_subtype {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a : α // p a }] :
      map (Function.Embedding.subtype p) univ = filter p univ
      source
      theorem Finset.univ_val_map_subtype_val {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a : α // p a }] :
      Multiset.map Subtype.val univ.val = (filter p univ).val
      source
      theorem Finset.univ_val_map_subtype_restrict {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) (p : α → Prop) [DecidablePred p] [Fintype { a : α // p a }] :
      Multiset.map (Subtype.restrict p f) univ.val = Multiset.map f (filter p univ).val
      source
      @[simp]
      theorem Finset.filter_univ_mem {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      {x : α | x ∈ s} = s
      source
      instance Finset.decidableCodisjoint {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
      Decidable (Codisjoint s t)
      Equations
        source
        instance Finset.decidableIsCompl {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
        Decidable (IsCompl s t)
        Equations