doc-next-gen

Mathlib.Data.Finset.BooleanAlgebra

Module docstring

{"# 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 "}
Finset.univ_nonempty theorem
[Nonempty α] : (univ : Finset α).Nonempty
Full source 
@[simp, aesop unsafe apply (rule_sets := [finsetNonempty])]
theorem univ_nonempty [Nonempty α] : (univ : Finset α).Nonempty :=
  univ_nonempty_iff.2 ‹_›
Nonemptiness of the Universal Finite Set for Nonempty Finite Types
Informal description
For any nonempty finite type $\alpha$, the universal finite set $\text{univ} : \text{Finset } \alpha$ is nonempty.
Finset.univ_nontrivial_iff theorem
: (Finset.univ : Finset α).Nontrivial ↔ Nontrivial α
Full source 
theorem univ_nontrivial_iff :
    (Finset.univ : Finset α).Nontrivial ↔ Nontrivial α := by
  rw [Finset.Nontrivial, Finset.coe_univ, Set.nontrivial_univ_iff]
Nontriviality of Universal Finite Set Equivalence
Informal description
For a finite type $\alpha$, the universal finite set $\text{Finset.univ}$ is nontrivial (contains at least two distinct elements) if and only if the type $\alpha$ itself is nontrivial (contains at least two distinct elements).
Finset.univ_nontrivial theorem
[h : Nontrivial α] : (Finset.univ : Finset α).Nontrivial
Full source 
theorem univ_nontrivial [h : Nontrivial α] :
    (Finset.univ : Finset α).Nontrivial :=
  univ_nontrivial_iff.mpr h
Nontriviality of the Universal Finite Set
Informal description
If the type $\alpha$ is nontrivial (i.e., contains at least two distinct elements), then the universal finite set $\text{Finset.univ}$ of $\alpha$ is also nontrivial (i.e., contains at least two distinct elements).
Finset.univ_eq_empty theorem
[IsEmpty α] : (univ : Finset α) = ∅
Full source 
@[simp]
theorem univ_eq_empty [IsEmpty α] : (univ : Finset α) = ∅ :=
  univ_eq_empty_iff.2 ‹_›
Universal Finite Set is Empty for Empty Type
Informal description
For any finite type $\alpha$ that is empty (i.e., $\alpha$ has no elements), the universal finite set $\text{univ}$ of $\alpha$ is equal to the empty set $\emptyset$.
Finset.univ_unique theorem
[Unique α] : (univ : Finset α) = { default }
Full source 
@[simp]
theorem univ_unique [Unique α] : (univ : Finset α) = {default} :=
  Finset.ext fun x => iff_of_true (mem_univ _) <| mem_singleton.2 <| Subsingleton.elim x default
Universal Finite Set of a Singleton Type is the Singleton of Default
Informal description
For a finite type $\alpha$ with a unique element (i.e., $\alpha$ is a singleton type), the universal finite set $\text{univ}$ is equal to the singleton set $\{\text{default}\}$, where $\text{default}$ is the unique element of $\alpha$.
Finset.boundedOrder instance
: BoundedOrder (Finset α)
Full source 
instance boundedOrder : BoundedOrder (Finset α) :=
  { inferInstanceAs (OrderBot (Finset α)) with
    top := univ
    le_top := subset_univ }
Bounded Order Structure on Finite Subsets
Informal description
For any finite type $\alpha$, the finite subsets of $\alpha$ form a bounded order, where the empty set $\emptyset$ is the least element and the universal set $\text{univ}$ (containing all elements of $\alpha$) is the greatest element.
Finset.top_eq_univ theorem
: (⊤ : Finset α) = univ
Full source 
@[simp]
theorem top_eq_univ : (⊤ : Finset α) = univ :=
  rfl
Top Element Equals Universal Set in Finite Subsets
Informal description
For any finite type $\alpha$, the top element in the partial order of finite subsets of $\alpha$ is equal to the universal finite set $\text{univ}$ containing all elements of $\alpha$.
Finset.ssubset_univ_iff theorem
{s : Finset α} : s ⊂ univ ↔ s ≠ univ
Full source 
theorem ssubset_univ_iff {s : Finset α} : s ⊂ univs ⊂ univ ↔ s ≠ univ :=
  @lt_top_iff_ne_top _ _ _ s
Characterization of Strict Subset of Universal Finite Set: $s \subset \text{univ} \leftrightarrow s \neq \text{univ}$
Informal description
For any finite subset $s$ of a finite type $\alpha$, $s$ is a strict subset of the universal set $\text{univ}$ (containing all elements of $\alpha$) if and only if $s$ is not equal to $\text{univ}$.
Finset.univ_subset_iff theorem
{s : Finset α} : univ ⊆ s ↔ s = univ
Full source 
@[simp]
theorem univ_subset_iff {s : Finset α} : univuniv ⊆ suniv ⊆ s ↔ s = univ :=
  @top_le_iff _ _ _ s
Universal Set Subset Characterization: $\text{univ} \subseteq s \leftrightarrow s = \text{univ}$
Informal description
For any finite subset $s$ of a finite type $\alpha$, the universal set $\text{univ}$ (containing all elements of $\alpha$) is a subset of $s$ if and only if $s$ is equal to $\text{univ}$.
Finset.codisjoint_left theorem
: Codisjoint s t ↔ ∀ ⦃a⦄, a ∉ s → a ∈ t
Full source 
theorem codisjoint_left : CodisjointCodisjoint s t ↔ ∀ ⦃a⦄, a ∉ s → a ∈ t := by
  classical simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]
Codisjointness Criterion for Finite Sets: Left Version
Informal description
For any two finite subsets $s$ and $t$ of a finite type $\alpha$, the elements $s$ and $t$ are codisjoint if and only if for every element $a \in \alpha$, if $a$ is not in $s$, then $a$ must be in $t$.
Finset.codisjoint_right theorem
: Codisjoint s t ↔ ∀ ⦃a⦄, a ∉ t → a ∈ s
Full source 
theorem codisjoint_right : CodisjointCodisjoint s t ↔ ∀ ⦃a⦄, a ∉ t → a ∈ s :=
  codisjoint_comm.trans codisjoint_left
Codisjointness Criterion for Finite Sets: Right Version
Informal description
For any two finite subsets $s$ and $t$ of a finite type $\alpha$, the elements $s$ and $t$ are codisjoint if and only if for every element $a \in \alpha$, if $a$ is not in $t$, then $a$ must be in $s$.
Finset.booleanAlgebra instance
[DecidableEq α] : BooleanAlgebra (Finset α)
Full source 
instance booleanAlgebra [DecidableEq α] : BooleanAlgebra (Finset α) :=
  GeneralizedBooleanAlgebra.toBooleanAlgebra
Boolean Algebra Structure on Finite Subsets of a Finite Type
Informal description
For any finite type $\alpha$ with decidable equality, the finite subsets of $\alpha$ form a Boolean algebra. In this structure: - The meet and join operations are intersection ($\cap$) and union ($\cup$) respectively - The complement operation is set complement ($(\cdot)^\complement$) - The top and bottom elements are the universal set $\text{univ}$ and empty set $\emptyset$ respectively - The difference operation $s \setminus t$ equals $s \cap t^\complement$
Finset.sdiff_eq_inter_compl theorem
(s t : Finset α) : s \ t = s ∩ tᶜ
Full source 
theorem sdiff_eq_inter_compl (s t : Finset α) : s \ t = s ∩ tᶜ :=
  sdiff_eq
Set Difference as Intersection with Complement in Finite Sets: $s \setminus t = s \cap t^\complement$
Informal description
For any finite subsets $s$ and $t$ of a type $\alpha$, the set difference $s \setminus t$ equals the intersection of $s$ with the complement of $t$, i.e., $s \setminus t = s \cap t^\complement$.
Finset.compl_eq_univ_sdiff theorem
(s : Finset α) : sᶜ = univ \ s
Full source 
theorem compl_eq_univ_sdiff (s : Finset α) : sᶜ = univuniv \ s :=
  rfl
Complement as Universal Set Difference for Finite Subsets
Informal description
For any finite subset $s$ of a finite type $\alpha$, the complement of $s$ equals the difference between the universal set $\text{univ}$ and $s$, i.e., $s^\complement = \text{univ} \setminus s$.
Finset.mem_compl theorem
: a ∈ sᶜ ↔ a ∉ s
Full source 
@[simp]
theorem mem_compl : a ∈ sᶜa ∈ sᶜ ↔ a ∉ s := by simp [compl_eq_univ_sdiff]
Characterization of Membership in Complement of Finite Set
Informal description
For any element $a$ of type $\alpha$ and any finite subset $s$ of $\alpha$, the element $a$ belongs to the complement of $s$ if and only if $a$ does not belong to $s$. In symbols: $$ a \in s^\complement \leftrightarrow a \notin s. $$
Finset.not_mem_compl theorem
: a ∉ sᶜ ↔ a ∈ s
Full source 
theorem not_mem_compl : a ∉ sᶜa ∉ sᶜ ↔ a ∈ s := by rw [mem_compl, not_not]
Complement Membership Characterization for Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite subset $s$ of $\alpha$, the element $a$ does not belong to the complement of $s$ if and only if $a$ belongs to $s$. In symbols: $$ a \notin s^\complement \leftrightarrow a \in s. $$
Finset.coe_compl theorem
(s : Finset α) : ↑sᶜ = (↑s : Set α)ᶜ
Full source 
@[simp, norm_cast]
theorem coe_compl (s : Finset α) : ↑sᶜ = (↑s : Set α)ᶜ :=
  Set.ext fun _ => mem_compl
Coercion of Finite Set Complement Equals Set Complement of Coercion
Informal description
For any finite subset $s$ of a type $\alpha$, the coercion of the complement of $s$ (as a `Finset`) to a set equals the complement of the coercion of $s$ to a set. In symbols: $$ (s^\complement : \text{Set } \alpha) = (s : \text{Set } \alpha)^\complement. $$
Finset.compl_subset_compl theorem
: sᶜ ⊆ tᶜ ↔ t ⊆ s
Full source 
@[simp] lemma compl_subset_compl : sᶜsᶜ ⊆ tᶜsᶜ ⊆ tᶜ ↔ t ⊆ s := @compl_le_compl_iff_le (Finset α) _ _ _
Order Reversal of Finite Set Complements: $s^\complement \subseteq t^\complement \leftrightarrow t \subseteq s$
Informal description
For any finite subsets $s$ and $t$ of a finite type $\alpha$, the complement of $s$ is a subset of the complement of $t$ if and only if $t$ is a subset of $s$. In symbols: $$ s^\complement \subseteq t^\complement \leftrightarrow t \subseteq s. $$
Finset.compl_ssubset_compl theorem
: sᶜ ⊂ tᶜ ↔ t ⊂ s
Full source 
@[simp] lemma compl_ssubset_compl : sᶜsᶜ ⊂ tᶜsᶜ ⊂ tᶜ ↔ t ⊂ s := @compl_lt_compl_iff_lt (Finset α) _ _ _
Strict Order Reversal of Finite Set Complements: $s^\complement \subset t^\complement \leftrightarrow t \subset s$
Informal description
For any finite subsets $s$ and $t$ of a finite type $\alpha$, the complement of $s$ is a strict subset of the complement of $t$ if and only if $t$ is a strict subset of $s$. In symbols: $$ s^\complement \subset t^\complement \leftrightarrow t \subset s. $$
Finset.subset_compl_comm theorem
: s ⊆ tᶜ ↔ t ⊆ sᶜ
Full source 
lemma subset_compl_comm : s ⊆ tᶜs ⊆ tᶜ ↔ t ⊆ sᶜ := le_compl_iff_le_compl (α := Finset α)
Subset-Complement Commutation for Finite Sets
Informal description
For any finite subsets $s$ and $t$ of a finite type $\alpha$, the subset relation $s \subseteq t^\complement$ holds if and only if $t \subseteq s^\complement$.
Finset.subset_compl_singleton theorem
: s ⊆ { a }ᶜ ↔ a ∉ s
Full source 
@[simp] lemma subset_compl_singleton : s ⊆ {a}ᶜs ⊆ {a}ᶜ ↔ a ∉ s := by
  rw [subset_compl_comm, singleton_subset_iff, mem_compl]
Subset-Complement-Singleton Criterion: $s \subseteq \{a\}^\complement \leftrightarrow a \notin s$
Informal description
For any finite subset $s$ of a finite type $\alpha$ and any element $a \in \alpha$, the subset relation $s \subseteq \{a\}^\complement$ holds if and only if $a$ does not belong to $s$.
Finset.compl_empty theorem
: (∅ : Finset α)ᶜ = univ
Full source 
@[simp]
theorem compl_empty : (∅ : Finset α)ᶜ = univ :=
  compl_bot
Complement of Empty Set is Universal Set in Finite Boolean Algebra
Informal description
The complement of the empty set in the Boolean algebra of finite subsets of a finite type $\alpha$ is equal to the universal set, i.e., $\emptyset^\complement = \text{univ}$.
Finset.compl_univ theorem
: (univ : Finset α)ᶜ = ∅
Full source 
@[simp]
theorem compl_univ : (univ : Finset α)ᶜ = ∅ :=
  compl_top
Complement of Universal Set is Empty in Finite Boolean Algebra
Informal description
In the Boolean algebra of finite subsets of a finite type $\alpha$, the complement of the universal set $\text{univ}$ is the empty set, i.e., $\text{univ}^\complement = \emptyset$.
Finset.compl_eq_empty_iff theorem
(s : Finset α) : sᶜ = ∅ ↔ s = univ
Full source 
@[simp]
theorem compl_eq_empty_iff (s : Finset α) : sᶜsᶜ = ∅ ↔ s = univ :=
  compl_eq_bot
Complement Characterization: $s^\complement = \emptyset \leftrightarrow s = \text{univ}$
Informal description
For any finite subset $s$ of a finite type $\alpha$, the complement of $s$ is the empty set if and only if $s$ is the universal set, i.e., $s^\complement = \emptyset \leftrightarrow s = \text{univ}$.
Finset.compl_eq_univ_iff theorem
(s : Finset α) : sᶜ = univ ↔ s = ∅
Full source 
@[simp]
theorem compl_eq_univ_iff (s : Finset α) : sᶜsᶜ = univ ↔ s = ∅ :=
  compl_eq_top
Complement Characterization: $s^\complement = \text{univ} \leftrightarrow s = \emptyset$
Informal description
For any finite subset $s$ of a finite type $\alpha$, the complement of $s$ equals the universal set if and only if $s$ is the empty set, i.e., $$s^\complement = \text{univ} \leftrightarrow s = \emptyset.$$
Finset.union_compl theorem
(s : Finset α) : s ∪ sᶜ = univ
Full source 
@[simp]
theorem union_compl (s : Finset α) : s ∪ sᶜ = univ :=
  sup_compl_eq_top
Union with Complement Yields Universal Set in Finite Subsets
Informal description
For any finite subset $s$ of a finite type $\alpha$, the union of $s$ with its complement $s^\complement$ equals the universal set $\text{univ}$ (the set containing all elements of $\alpha$), i.e., $s \cup s^\complement = \text{univ}$.
Finset.inter_compl theorem
(s : Finset α) : s ∩ sᶜ = ∅
Full source 
@[simp]
theorem inter_compl (s : Finset α) : s ∩ sᶜ = ∅ :=
  inf_compl_eq_bot
Intersection with Complement Yields Empty Set for Finite Subsets
Informal description
For any finite subset $s$ of a finite type $\alpha$, the intersection of $s$ with its complement is the empty set, i.e., $s \cap s^\complement = \emptyset$.
Finset.compl_union theorem
(s t : Finset α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ
Full source 
@[simp]
theorem compl_union (s t : Finset α) : (s ∪ t)ᶜ = sᶜsᶜ ∩ tᶜ :=
  compl_sup
De Morgan's Law for Finite Sets: $(s \cup t)^\complement = s^\complement \cap t^\complement$
Informal description
For any finite subsets $s$ and $t$ of a finite type $\alpha$ with decidable equality, the complement of their union equals the intersection of their complements, i.e., $(s \cup t)^\complement = s^\complement \cap t^\complement$.
Finset.compl_inter theorem
(s t : Finset α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ
Full source 
@[simp]
theorem compl_inter (s t : Finset α) : (s ∩ t)ᶜ = sᶜsᶜ ∪ tᶜ :=
  compl_inf
De Morgan's Law for Complements of Finite Set Intersections: $(s \cap t)^\complement = s^\complement \cup t^\complement$
Informal description
For any finite subsets $s$ and $t$ of a finite type $\alpha$ with decidable equality, the complement of their intersection equals the union of their complements, i.e., $$(s \cap t)^\complement = s^\complement \cup t^\complement.$$
Finset.compl_erase theorem
: (s.erase a)ᶜ = insert a sᶜ
Full source 
@[simp]
theorem compl_erase : (s.erase a)ᶜ = insert a sᶜ := by
  ext
  simp only [or_iff_not_imp_left, mem_insert, not_and, mem_compl, mem_erase]
Complement of Set Erasure Equals Insertion into Complement: $(s \setminus \{a\})^\complement = \{a\} \cup s^\complement$
Informal description
For any finite subset $s$ of a finite type $\alpha$ with decidable equality and any element $a \in \alpha$, the complement of the set obtained by removing $a$ from $s$ equals the set obtained by inserting $a$ into the complement of $s$, i.e., $$(s \setminus \{a\})^\complement = \{a\} \cup s^\complement.$$
Finset.compl_insert theorem
: (insert a s)ᶜ = sᶜ.erase a
Full source 
@[simp]
theorem compl_insert : (insert a s)ᶜ = sᶜ.erase a := by
  ext
  simp only [not_or, mem_insert, mem_compl, mem_erase]
Complement of Insertion Equals Erasure of Complement
Informal description
For any finite subset $s$ of a finite type $\alpha$ with decidable equality and any element $a \in \alpha$, the complement of the set obtained by inserting $a$ into $s$ equals the set obtained by removing $a$ from the complement of $s$, i.e., $$(\{a\} \cup s)^\complement = s^\complement \setminus \{a\}.$$
Finset.insert_compl_insert theorem
(ha : a ∉ s) : insert a (insert a s)ᶜ = sᶜ
Full source 
theorem insert_compl_insert (ha : a ∉ s) : insert a (insert a s)ᶜ = sᶜ := by
  simp_rw [compl_insert, insert_erase (mem_compl.2 ha)]
Double Insertion-Complement Identity for Finite Sets
Informal description
For any finite subset $s$ of a finite type $\alpha$ with decidable equality and any element $a \notin s$, the insertion of $a$ into the complement of the set obtained by inserting $a$ into $s$ equals the complement of $s$, i.e., $$\{a\} \cup (\{a\} \cup s)^\complement = s^\complement.$$
Finset.insert_compl_self theorem
(x : α) : insert x ({ x }ᶜ : Finset α) = univ
Full source 
@[simp]
theorem insert_compl_self (x : α) : insert x ({x}{x}ᶜ : Finset α) = univ := by
  rw [← compl_erase, erase_singleton, compl_empty]
Insertion of Element with its Complement Forms Universal Set
Informal description
For any element $x$ of a finite type $\alpha$, the union of $\{x\}$ with the complement of $\{x\}$ equals the universal set, i.e., $\{x\} \cup \{x\}^\complement = \text{univ}$.
Finset.compl_filter theorem
(p : α → Prop) [DecidablePred p] [∀ x, Decidable ¬p x] : (univ.filter p)ᶜ = univ.filter fun x => ¬p x
Full source 
@[simp]
theorem compl_filter (p : α → Prop) [DecidablePred p] [∀ x, Decidable ¬p x] :
    (univ.filter p)ᶜ = univ.filter fun x => ¬p x :=
  ext <| by simp
Complement of Filtered Universal Set Equals Filter of Negated Predicate
Informal description
For any decidable predicate $p : \alpha \to \text{Prop}$ on a finite type $\alpha$, the complement of the finite subset of $\alpha$ consisting of elements satisfying $p$ is equal to the finite subset of $\alpha$ consisting of elements not satisfying $p$. In other words, $$(\text{univ.filter } p)^\complement = \text{univ.filter } (\lambda x, \neg p x).$$
Finset.compl_ne_univ_iff_nonempty theorem
(s : Finset α) : sᶜ ≠ univ ↔ s.Nonempty
Full source 
theorem compl_ne_univ_iff_nonempty (s : Finset α) : sᶜsᶜ ≠ univsᶜ ≠ univ ↔ s.Nonempty := by
  simp [eq_univ_iff_forall, Finset.Nonempty]
Complement of Finite Set Not Universal iff Nonempty
Informal description
For any finite subset $s$ of a finite type $\alpha$, the complement of $s$ is not equal to the universal set if and only if $s$ is nonempty. In other words, $s^\complement \neq \text{univ} \iff s \neq \emptyset$.
Finset.compl_singleton theorem
(a : α) : ({ a } : Finset α)ᶜ = univ.erase a
Full source 
theorem compl_singleton (a : α) : ({a} : Finset α)ᶜ = univ.erase a := by
  rw [compl_eq_univ_sdiff, sdiff_singleton_eq_erase]
Complement of Singleton Equals Universal Set Minus Element
Informal description
For any element $a$ of a finite type $\alpha$, the complement of the singleton set $\{a\}$ in the finite subsets of $\alpha$ is equal to the universal finite set with $a$ removed, i.e., $\{a\}^\complement = \text{univ} \setminus \{a\}$.
Finset.insert_inj_on' theorem
(s : Finset α) : Set.InjOn (fun a => insert a s) (sᶜ : Finset α)
Full source 
theorem insert_inj_on' (s : Finset α) : Set.InjOn (fun a => insert a s) (sᶜ : Finset α) := by
  rw [coe_compl]
  exact s.insert_inj_on
Injectivity of Insertion on Complement of Finite Set
Informal description
For any finite subset $s$ of a type $\alpha$, the function $a \mapsto \{a\} \cup s$ is injective on the complement of $s$ (viewed as a finite set).
Finset.image_univ_of_surjective theorem
[Fintype β] {f : β → α} (hf : Surjective f) : univ.image f = univ
Full source 
theorem image_univ_of_surjective [Fintype β] {f : β → α} (hf : Surjective f) :
    univ.image f = univ :=
  eq_univ_of_forall <| hf.forall.2 fun _ => mem_image_of_mem _ <| mem_univ _
Surjective Function Maps Universal Set to Universal Set
Informal description
Let $\alpha$ and $\beta$ be finite types, and let $f : \beta \to \alpha$ be a surjective function. Then the image of the universal finite set of $\beta$ under $f$ is equal to the universal finite set of $\alpha$, i.e., $f(\text{univ}) = \text{univ}$.
Finset.image_univ_equiv theorem
[Fintype β] (f : β ≃ α) : univ.image f = univ
Full source 
@[simp]
theorem image_univ_equiv [Fintype β] (f : β ≃ α) : univ.image f = univ :=
  Finset.image_univ_of_surjective f.surjective
Image of Universal Set under Equivalence is Universal Set
Informal description
For any finite types $\alpha$ and $\beta$, and any equivalence (bijection) $f : \beta \simeq \alpha$, the image of the universal finite set of $\beta$ under $f$ equals the universal finite set of $\alpha$, i.e., $f(\text{univ}) = \text{univ}$.
Finset.univ_inter theorem
(s : Finset α) : univ ∩ s = s
Full source 
@[simp] lemma univ_inter (s : Finset α) : univuniv ∩ s = s := by ext a; simp
Intersection with Universal Set Preserves Finite Set
Informal description
For any finite set $s$ of a finite type $\alpha$, the intersection of the universal finite set (containing all elements of $\alpha$) with $s$ equals $s$ itself, i.e., $\text{univ} \cap s = s$.
Finset.inter_univ theorem
(s : Finset α) : s ∩ univ = s
Full source 
@[simp] lemma inter_univ (s : Finset α) : s ∩ univ = s := by rw [inter_comm, univ_inter]
Intersection with Universal Set Preserves Finite Set (Right Version)
Informal description
For any finite set $s$ of a finite type $\alpha$, the intersection of $s$ with the universal finite set (containing all elements of $\alpha$) equals $s$ itself, i.e., $s \cap \text{univ} = s$.
Finset.inter_eq_univ theorem
: s ∩ t = univ ↔ s = univ ∧ t = univ
Full source 
@[simp] lemma inter_eq_univ : s ∩ ts ∩ t = univ ↔ s = univ ∧ t = univ := inf_eq_top_iff
Intersection Equals Universal Set iff Both Sets Are Universal
Informal description
For any finite sets $s$ and $t$ of a finite type $\alpha$, the intersection $s \cap t$ equals the universal set $\text{univ}$ (containing all elements of $\alpha$) if and only if both $s$ and $t$ equal $\text{univ}$.
Finset.singleton_eq_univ theorem
[Subsingleton α] (a : α) : ({ a } : Finset α) = univ
Full source 
lemma singleton_eq_univ [Subsingleton α] (a : α) : ({a} : Finset α) = univ := by
  ext b; simp [Subsingleton.elim a b]
Singleton Equals Universal Set in Subsingleton Types
Informal description
For any type $\alpha$ with at most one distinct element (i.e., a subsingleton), and for any element $a \in \alpha$, the singleton set $\{a\}$ is equal to the universal finite set containing all elements of $\alpha$.
Finset.map_univ_of_surjective theorem
[Fintype β] {f : β ↪ α} (hf : Surjective f) : univ.map f = univ
Full source 
theorem map_univ_of_surjective [Fintype β] {f : β ↪ α} (hf : Surjective f) : univ.map f = univ :=
  eq_univ_of_forall <| hf.forall.2 fun _ => mem_map_of_mem _ <| mem_univ _
Image of Universal Set under Bijective Embedding Equals Universal Set
Informal description
Let $\alpha$ and $\beta$ be finite types, and let $f : \beta \hookrightarrow \alpha$ be an injective embedding that is also surjective. Then the image of the universal finite set of $\beta$ under $f$ is equal to the universal finite set of $\alpha$, i.e., $$ \text{map}(f)(\text{univ}) = \text{univ}. $$
Finset.map_univ_equiv theorem
[Fintype β] (f : β ≃ α) : univ.map f.toEmbedding = univ
Full source 
@[simp]
theorem map_univ_equiv [Fintype β] (f : β ≃ α) : univ.map f.toEmbedding = univ :=
  map_univ_of_surjective f.surjective
Universal Set Preservation under Bijective Embedding
Informal description
For any finite types $\alpha$ and $\beta$, and any equivalence (bijection) $f : \beta \simeq \alpha$, the image of the universal finite set of $\beta$ under the injective embedding induced by $f$ is equal to the universal finite set of $\alpha$. That is: $$ \text{map}(f.\text{toEmbedding})(\text{univ}_\beta) = \text{univ}_\alpha $$ where $\text{univ}_\beta$ and $\text{univ}_\alpha$ denote the universal finite sets containing all elements of $\beta$ and $\alpha$ respectively.
Finset.univ_map_equiv_to_embedding theorem
{α β : Type*} [Fintype α] [Fintype β] (e : α ≃ β) : univ.map e.toEmbedding = univ
Full source 
theorem univ_map_equiv_to_embedding {α β : Type*} [Fintype α] [Fintype β] (e : α ≃ β) :
    univ.map e.toEmbedding = univ :=
  eq_univ_iff_forall.mpr fun b => mem_map.mpr ⟨e.symm b, mem_univ _, by simp⟩
Image of Universal Set under Equivalence Embedding Equals Universal Set
Informal description
For any finite types $\alpha$ and $\beta$, and any equivalence (bijection) $e : \alpha \simeq \beta$, the image of the universal finite set of $\alpha$ under the injective embedding induced by $e$ is equal to the universal finite set of $\beta$. In other words: $$ \text{map}(e.\text{toEmbedding})(\text{univ}) = \text{univ} $$
Finset.univ_filter_exists theorem
(f : α → β) [Fintype β] [DecidablePred fun y => ∃ x, f x = y] [DecidableEq β] : (Finset.univ.filter fun y => ∃ x, f x = y) = Finset.univ.image f
Full source 
@[simp]
theorem univ_filter_exists (f : α → β) [Fintype β] [DecidablePred fun y => ∃ x, f x = y]
    [DecidableEq β] : (Finset.univ.filter fun y => ∃ x, f x = y) = Finset.univ.image f := by
  ext
  simp
Image of Universal Set Equals Filtered Preimage Set for Finite Types
Informal description
Let $f : \alpha \to \beta$ be a function between finite types $\alpha$ and $\beta$, with a decidable predicate for the existence of preimages and decidable equality on $\beta$. Then the finite subset of $\beta$ consisting of elements $y$ for which there exists an $x$ such that $f(x) = y$ is equal to the image of the universal finite set under $f$. In other words: $$\{y \in \beta \mid \exists x \in \alpha, f(x) = y\} = f(\text{univ})$$ where $\text{univ}$ denotes the universal finite set containing all elements of $\alpha$.
Finset.univ_filter_mem_range theorem
(f : α → β) [Fintype β] [DecidablePred fun y => y ∈ Set.range f] [DecidableEq β] : (Finset.univ.filter fun y => y ∈ Set.range f) = Finset.univ.image f
Full source 
/-- Note this is a special case of `(Finset.image_preimage f univ _).symm`. -/
theorem univ_filter_mem_range (f : α → β) [Fintype β] [DecidablePred fun y => y ∈ Set.range f]
    [DecidableEq β] : (Finset.univ.filter fun y => y ∈ Set.range f) = Finset.univ.image f := by
  letI : DecidablePred (fun y => ∃ x, f x = y) := by simpa using ‹_›
  exact univ_filter_exists f
Range of Function on Finite Types Equals Image of Universal Set
Informal description
Let $\alpha$ and $\beta$ be finite types, and let $f : \alpha \to \beta$ be a function with decidable range membership and decidable equality on $\beta$. Then the finite subset of $\beta$ consisting of elements in the range of $f$ is equal to the image of the universal finite set under $f$. In other words: $$\{y \in \beta \mid y \in \text{range } f\} = f(\text{univ})$$ where $\text{univ}$ denotes the universal finite set containing all elements of $\alpha$.
Finset.coe_filter_univ theorem
(p : α → Prop) [DecidablePred p] : (univ.filter p : Set α) = {x | p x}
Full source 
theorem coe_filter_univ (p : α → Prop) [DecidablePred p] :
    (univ.filter p : Set α) = { x | p x } := by simp
Set Correspondence of Filtered Universal Finite Set: $\overline{\text{univ.filter}\,p} = \{x \mid p x\}$
Informal description
For any decidable predicate $p : \alpha \to \text{Prop}$ on a finite type $\alpha$, the set corresponding to the filtered universal finite set $\text{univ.filter}\,p$ is equal to the set $\{x \mid p x\}$ of all elements satisfying $p$.
Finset.subtype_eq_univ theorem
{p : α → Prop} [DecidablePred p] [Fintype { a // p a }] : s.subtype p = univ ↔ ∀ ⦃a⦄, p a → a ∈ s
Full source 
@[simp] lemma subtype_eq_univ {p : α → Prop} [DecidablePred p] [Fintype {a // p a}] :
    s.subtype p = univ ↔ ∀ ⦃a⦄, p a → a ∈ s := by simp [Finset.ext_iff]
Characterization of When Subtype of Finite Set Equals Universal Set
Informal description
Let $\alpha$ be a finite type, $s$ be a finite subset of $\alpha$, and $p : \alpha \to \text{Prop}$ be a decidable predicate. Then the subtype of $s$ with respect to $p$ equals the universal finite set of $\{a \mid p a\}$ if and only if every element of $\alpha$ satisfying $p$ is contained in $s$. In other words: $$ s.\text{subtype}\ p = \text{univ} \leftrightarrow \forall a \in \alpha,\ p a \to a \in s. $$
Finset.subtype_univ theorem
[Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] : univ.subtype p = univ
Full source 
@[simp] lemma subtype_univ [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype {a // p a}] :
    univ.subtype p = univ := by simp
Universal subtype of a finite type equals universal set of the subtype
Informal description
For a finite type $\alpha$ and a decidable predicate $p : \alpha \to \text{Prop}$, if the subtype $\{a \mid p a\}$ is also finite, then the finite set of all elements of this subtype (constructed from the universal finite set of $\alpha$) is equal to the universal finite set of the subtype. In other words, $\text{univ.subtype } p = \text{univ}$ under the given finiteness conditions.
Finset.univ_map_subtype theorem
[Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] : univ.map (Function.Embedding.subtype p) = univ.filter p
Full source 
lemma univ_map_subtype [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype {a // p a}] :
    univ.map (Function.Embedding.subtype p) = univ.filter p := by
  rw [← subtype_map, subtype_univ]
Image of Universal Subtype Equals Filtered Universal Set: $\text{univ.map } (\text{subtype } p) = \text{univ.filter } p$
Informal description
For a finite type $\alpha$ and a decidable predicate $p : \alpha \to \text{Prop}$, if the subtype $\{a \mid p a\}$ is also finite, then the image of the universal finite set of this subtype under the inclusion embedding $\{a \mid p a\} \hookrightarrow \alpha$ is equal to the filtered finite set $\text{univ.filter } p$. In other words, $\text{univ.map } (\text{subtype } p) = \text{univ.filter } p$ under the given finiteness conditions.
Finset.univ_val_map_subtype_val theorem
[Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] : univ.val.map ((↑) : { a // p a } → α) = (univ.filter p).val
Full source 
lemma univ_val_map_subtype_val [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype {a // p a}] :
    univ.val.map ((↑) : { a // p a } → α) = (univ.filter p).val := by
  apply (map_val (Function.Embedding.subtype p) univ).symm.trans
  apply congr_arg
  apply univ_map_subtype
Multiset Equality for Subtype Inclusion and Filtered Universal Set
Informal description
For a finite type $\alpha$ and a decidable predicate $p : \alpha \to \text{Prop}$, if the subtype $\{a \mid p a\}$ is also finite, then the multiset obtained by applying the inclusion map to all elements of the universal finite set of the subtype is equal to the underlying multiset of the filtered universal finite set of $\alpha$ by $p$. In other words, $\text{univ.val.map } (\text{subtype } p) = (\text{univ.filter } p).val$ under the given finiteness conditions.
Finset.univ_val_map_subtype_restrict theorem
[Fintype α] (f : α → β) (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] : univ.val.map (Subtype.restrict p f) = (univ.filter p).val.map f
Full source 
lemma univ_val_map_subtype_restrict [Fintype α] (f : α → β)
    (p : α → Prop) [DecidablePred p] [Fintype {a // p a}] :
    univ.val.map (Subtype.restrict p f) = (univ.filter p).val.map f := by
  rw [← univ_val_map_subtype_val, Multiset.map_map, Subtype.restrict_def]
Multiset Equality for Restricted Function and Filtered Universal Set
Informal description
For a finite type $\alpha$, a function $f \colon \alpha \to \beta$, and a decidable predicate $p \colon \alpha \to \text{Prop}$ such that the subtype $\{a \mid p a\}$ is finite, the multiset obtained by applying the restricted function $\text{Subtype.restrict } p \ f$ to all elements of the universal finite set of the subtype is equal to the multiset obtained by applying $f$ to the underlying elements of the filtered universal finite set of $\alpha$ by $p$. In other words, $\text{univ.val.map } (\text{Subtype.restrict } p \ f) = (\text{univ.filter } p).\text{val.map } f$.
Finset.filter_univ_mem theorem
(s : Finset α) : univ.filter (· ∈ s) = s
Full source 
@[simp]
lemma filter_univ_mem (s : Finset α) : univ.filter (· ∈ s) = s := by simp [filter_mem_eq_inter]
Filtering the Universal Set by Membership in $s$ Yields $s$
Informal description
For any finite set $s$ of a finite type $\alpha$, the filtered set $\{x \in \text{univ} \mid x \in s\}$ is equal to $s$, where $\text{univ}$ denotes the universal finite set containing all elements of $\alpha$.
Finset.decidableCodisjoint instance
: Decidable (Codisjoint s t)
Full source 
instance decidableCodisjoint : Decidable (Codisjoint s t) :=
  decidable_of_iff _ codisjoint_left.symm
Decidability of Codisjointness for Finite Sets
Informal description
For any two finite subsets $s$ and $t$ of a finite type $\alpha$, it is decidable whether $s$ and $t$ are codisjoint, meaning their union is the universal set $\text{univ}$.
Finset.decidableIsCompl instance
: Decidable (IsCompl s t)
Full source 
instance decidableIsCompl : Decidable (IsCompl s t) :=
  decidable_of_iff' _ isCompl_iff
Boolean Algebra Structure on Finite Subsets of a Finite Type
Informal description
For any finite type $\alpha$, the collection of finite subsets of $\alpha$ forms a Boolean algebra. In this structure, the operations of union, intersection, and complement correspond to the usual set operations, the empty set $\emptyset$ is the bottom element, and the universal set $\text{univ}$ (containing all elements of $\alpha$) is the top element. Moreover, any two finite subsets $s$ and $t$ are complements if and only if their union is $\text{univ}$ and their intersection is $\emptyset$.