`Finset`s 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

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 α)

Equations

Finset.boundedOrder = { top := Finset.univ, le_top := ⋯, toOrderBot := inferInstance }

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 α)

Equations

Finset.booleanAlgebra = GeneralizedBooleanAlgebra.toBooleanAlgebra

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)

Equations

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

source

@[instance_reducible]

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) ⋯

Documentation

Mathlib.Data.Finset.BooleanAlgebra

`Finset`s are a Boolean algebra #

Main results #

Finsets are a Boolean algebra #

Main results #

`Finset`s are a Boolean algebra #