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_neq_empty (α : Type u_3) [Fintype α] [Nonempty α] :
univ ≠ ∅
source
theorem Finset.univ_nontrivial {α : Type u_1} [Fintype α] [h : Nontrivial α] :
univ.Nontrivial
source
@[simp]
theorem Finset.singleton_ne_univ {α : Type u_1} [Fintype α] [Nontrivial α] (a : α) :
{a} ≠ univ
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_reducible]
instance Finset.boundedOrder {α : Type u_1} [Fintype α] :
BoundedOrder (Finset α)
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_reducible]
instance Finset.booleanAlgebra {α : Type u_1} [Fintype α] [DecidableEq α] :
BooleanAlgebra (Finset α)
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
@[simp]
theorem Finset.mem_himp_iff {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] {a : α} :
a ∈ s ⇨ t ↔ a ∈ s → a ∈ t
source
theorem Finset.himp_def {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
s ⇨ t = t ∪ sᶜ
source
@[simp]
theorem Finset.mem_bihimp_iff {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] {a : α} :
a ∈ bihimp s t ↔ (a ∈ s ↔ a ∈ t)
source
theorem Finset.bihimp_def {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
bihimp s t = (s ∪ tᶜ) ∩ (t ∪ sᶜ)
source
@[simp]
theorem Finset.coe_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
↑sᶜ = (↑s)ᶜ
source
theorem Finset.compl_subset_compl {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
sᶜ ⊆ tᶜ ↔ t ⊆ s
source
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
theorem Finset.subset_compl_iff_disjoint_right {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
s ⊆ tᶜ ↔ Disjoint s t
source
theorem Finset.subset_compl_iff_disjoint_left {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
s ⊆ tᶜ ↔ Disjoint 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_3} {β : Type u_4} [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
theorem Finset.filter_univ_mem {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
{x : α | x ∈ s} = s
source
@[instance_reducible]
instance Finset.decidableCodisjoint {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
Decidable (Codisjoint s t)
source
@[instance_reducible]
instance Finset.decidableIsCompl {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] :
Decidable (IsCompl s t)