Finsets are a boolean algebra

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

Main results

• Finset.boundedOrder: Finset.univ is the top element of Finset α
• Finset.booleanAlgebra: Finset α is a boolean algebra if α is finite

theorem Finset.Nonempty.eq_univ {α : Type u_1} {s : Finset α} [Fintype α] [Subsingleton α] : s.Nonempty → s = univ

theorem Finset.univ_nonempty_iff {α : Type u_1} [Fintype α] : univ.Nonempty ↔ Nonempty α

@[simp]

theorem Finset.univ_nonempty {α : Type u_1} [Fintype α] [Nonempty α] : univ.Nonempty

theorem Finset.univ_eq_empty_iff {α : Type u_1} [Fintype α] : univ = ∅ ↔ IsEmpty α

theorem Finset.univ_nontrivial_iff {α : Type u_1} [Fintype α] : univ.Nontrivial ↔ Nontrivial α

theorem Finset.univ_nontrivial {α : Type u_1} [Fintype α] [h : Nontrivial α] : univ.Nontrivial

@[simp]

theorem Finset.univ_eq_empty {α : Type u_1} [Fintype α] [IsEmpty α] : univ = ∅

@[simp]

theorem Finset.univ_unique {α : Type u_1} [Fintype α] [Unique α] : univ = {default}

instance Finset.boundedOrder {α : Type u_1} [Fintype α] : BoundedOrder (Finset α)

Equations

• Finset.boundedOrder = BoundedOrder.mk

@[simp]

theorem Finset.top_eq_univ {α : Type u_1} [Fintype α] : ⊤ = univ

theorem Finset.ssubset_univ_iff {α : Type u_1} [Fintype α] {s : Finset α} : s ⊂ univ ↔ s ≠ univ

@[simp]

theorem Finset.univ_subset_iff {α : Type u_1} [Fintype α] {s : Finset α} : univ ⊆ s ↔ s = univ

theorem Finset.codisjoint_left {α : Type u_1} {s t : Finset α} [Fintype α] : Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t

theorem Finset.codisjoint_right {α : Type u_1} {s t : Finset α} [Fintype α] : Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∈ s

instance Finset.booleanAlgebra {α : Type u_1} [Fintype α] [DecidableEq α] : BooleanAlgebra (Finset α)

Equations

• Finset.booleanAlgebra = GeneralizedBooleanAlgebra.toBooleanAlgebra

theorem Finset.sdiff_eq_inter_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s t : Finset α) : s \ t = s ∩ tᶜ

theorem Finset.compl_eq_univ_sdiff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : sᶜ = univ \ s

@[simp]

theorem Finset.mem_compl {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} : a ∈ sᶜ ↔ a ∉ s

theorem Finset.not_mem_compl {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} : a ∉ sᶜ ↔ a ∈ s

@[simp]

theorem Finset.coe_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : ↑sᶜ = (↑s)ᶜ

@[simp]

theorem Finset.compl_subset_compl {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] : sᶜ ⊆ tᶜ ↔ t ⊆ s

@[simp]

theorem Finset.compl_ssubset_compl {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] : sᶜ ⊂ tᶜ ↔ t ⊂ s

theorem Finset.subset_compl_comm {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] : s ⊆ tᶜ ↔ t ⊆ sᶜ

@[simp]

theorem Finset.subset_compl_singleton {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} : s ⊆ {a}ᶜ ↔ a ∉ s

@[simp]

theorem Finset.compl_empty {α : Type u_1} [Fintype α] [DecidableEq α] : ∅ᶜ = univ

@[simp]

theorem Finset.compl_univ {α : Type u_1} [Fintype α] [DecidableEq α] : univᶜ = ∅

@[simp]

theorem Finset.compl_eq_empty_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : sᶜ = ∅ ↔ s = univ

@[simp]

theorem Finset.compl_eq_univ_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : sᶜ = univ ↔ s = ∅

@[simp]

theorem Finset.union_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : s ∪ sᶜ = univ

@[simp]

theorem Finset.inter_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : s ∩ sᶜ = ∅

@[simp]

theorem Finset.compl_union {α : Type u_1} [Fintype α] [DecidableEq α] (s t : Finset α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ

@[simp]

theorem Finset.compl_inter {α : Type u_1} [Fintype α] [DecidableEq α] (s t : Finset α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ

@[simp]

theorem Finset.compl_erase {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} : (s.erase a)ᶜ = insert a sᶜ

@[simp]

theorem Finset.compl_insert {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} : (insert a s)ᶜ = sᶜ.erase a

theorem Finset.insert_compl_insert {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] {a : α} (ha : a ∉ s) : insert a (insert a s)ᶜ = sᶜ

@[simp]

theorem Finset.insert_compl_self {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) : insert x {x}ᶜ = univ

@[simp]

theorem Finset.compl_filter {α : Type u_1} [Fintype α] [DecidableEq α] (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] : (filter p univ)ᶜ = filter (fun (x : α) => ¬p x) univ

theorem Finset.compl_ne_univ_iff_nonempty {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : sᶜ ≠ univ ↔ s.Nonempty

theorem Finset.compl_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (a : α) : {a}ᶜ = univ.erase a

theorem Finset.insert_inj_on' {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : Set.InjOn (fun (a : α) => insert a s) ↑sᶜ

theorem Finset.image_univ_of_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] {f : β → α} (hf : Function.Surjective f) : image f univ = univ

@[simp]

theorem Finset.image_univ_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] (f : β ≃ α) : image (⇑f) univ = univ

@[simp]

theorem Finset.univ_inter {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : univ ∩ s = s

@[simp]

theorem Finset.inter_univ {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : s ∩ univ = s

@[simp]

theorem Finset.inter_eq_univ {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] : s ∩ t = univ ↔ s = univ ∧ t = univ

theorem Finset.singleton_eq_univ {α : Type u_1} [Fintype α] [Subsingleton α] (a : α) : {a} = univ

theorem Finset.map_univ_of_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : β ↪ α} (hf : Function.Surjective ⇑f) : map f univ = univ

@[simp]

theorem Finset.map_univ_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : β ≃ α) : map f.toEmbedding univ = univ

theorem Finset.univ_map_equiv_to_embedding {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (e : α ≃ β) : map e.toEmbedding univ = univ

@[simp]

theorem Finset.univ_filter_exists {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) [Fintype β] [DecidablePred fun (y : β) => ∃ (x : α), f x = y] [DecidableEq β] : filter (fun (y : β) => ∃ (x : α), f x = y) univ = image f univ

theorem Finset.univ_filter_mem_range {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) [Fintype β] [DecidablePred fun (y : β) => y ∈ Set.range f] [DecidableEq β] : filter (fun (y : β) => y ∈ Set.range f) univ = image f univ

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

theorem Finset.coe_filter_univ {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] : ↑(filter p univ) = {x : α | p x}

@[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

@[simp]

theorem Finset.subtype_univ {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a : α // p a }] : Finset.subtype p univ = univ

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

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

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

@[simp]

theorem Finset.filter_univ_mem {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : filter (fun (x : α) => x ∈ s) univ = s

instance Finset.decidableCodisjoint {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] : Decidable (Codisjoint s t)

Equations

• Finset.decidableCodisjoint = decidable_of_iff (∀ ⦃a : α⦄, a ∉ s → a ∈ t) ⋯

instance Finset.decidableIsCompl {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] : Decidable (IsCompl s t)

Equations

• Finset.decidableIsCompl = decidable_of_iff' (Disjoint s t ∧ Codisjoint s t) ⋯