Mathlib.Data.Finset.Lattice.Lemmas

Finset.disjoint_iff_inter_eq_empty theorem

: Disjoint s t ↔ s ∩ t = ∅

Full source

theorem disjoint_iff_inter_eq_empty : DisjointDisjoint s t ↔ s ∩ t = ∅ :=
  disjoint_iff

Disjointness Criterion for Finite Sets: $s \cap t = \emptyset$

Informal description

Two finite sets $s$ and $t$ are disjoint if and only if their intersection is the empty set, i.e., $s \cap t = \emptyset$.

Finset.union_empty theorem

(s : Finset α) : s ∪ ∅ = s

Full source

@[simp]
theorem union_empty (s : Finset α) : s ∪ ∅ = s :=
  ext fun x => mem_union.trans <| by simp

Right Identity of Union with Empty Set in Finite Sets

Informal description

For any finite set $s$ of type $\alpha$, the union of $s$ with the empty set equals $s$, i.e., $s \cup \emptyset = s$.

Finset.empty_union theorem

(s : Finset α) : ∅ ∪ s = s

Full source

@[simp]
theorem empty_union (s : Finset α) : ∅∅ ∪ s = s :=
  ext fun x => mem_union.trans <| by simp

Left Identity of Union with Empty Set in Finite Sets

Informal description

For any finite set $s$ of type $\alpha$, the union of the empty set with $s$ equals $s$, i.e., $\emptyset \cup s = s$.

Finset.Nonempty.inl theorem

{s t : Finset α} (h : s.Nonempty) : (s ∪ t).Nonempty

Full source

@[aesop unsafe apply (rule_sets := [finsetNonempty])]
theorem Nonempty.inl {s t : Finset α} (h : s.Nonempty) : (s ∪ t).Nonempty :=
  h.mono subset_union_left

Nonempty Left Set Implies Nonempty Union

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, if $s$ is nonempty, then the union $s \cup t$ is also nonempty.

Finset.Nonempty.inr theorem

{s t : Finset α} (h : t.Nonempty) : (s ∪ t).Nonempty

Full source

@[aesop unsafe apply (rule_sets := [finsetNonempty])]
theorem Nonempty.inr {s t : Finset α} (h : t.Nonempty) : (s ∪ t).Nonempty :=
  h.mono subset_union_right

Nonempty Right Set Implies Nonempty Union

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, if $t$ is nonempty, then the union $s \cup t$ is also nonempty.

Finset.insert_eq theorem

(a : α) (s : Finset α) : insert a s = { a } ∪ s

Full source

theorem insert_eq (a : α) (s : Finset α) : insert a s = {a}{a} ∪ s :=
  rfl

Insertion as Union with Singleton

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, the insertion of $a$ into $s$ is equal to the union of the singleton set $\{a\}$ with $s$, i.e., $\text{insert } a s = \{a\} \cup s$.

Finset.insert_union theorem

(a : α) (s t : Finset α) : insert a s ∪ t = insert a (s ∪ t)

Full source

@[simp]
theorem insert_union (a : α) (s t : Finset α) : insertinsert a s ∪ t = insert a (s ∪ t) := by
  simp only [insert_eq, union_assoc]

Insertion-Union Distributivity for Finite Sets

Informal description

For any element $a$ of type $\alpha$ and any finite sets $s$ and $t$ of elements of $\alpha$, the union of the insertion of $a$ into $s$ with $t$ is equal to the insertion of $a$ into the union of $s$ and $t$, i.e., $$ (\{a\} \cup s) \cup t = \{a\} \cup (s \cup t). $$

Finset.union_insert theorem

(a : α) (s t : Finset α) : s ∪ insert a t = insert a (s ∪ t)

Full source

@[simp]
theorem union_insert (a : α) (s t : Finset α) : s ∪ insert a t = insert a (s ∪ t) := by
  simp only [insert_eq, union_left_comm]

Union with Insertion Equals Insertion of Union for Finite Sets

Informal description

For any element $a$ of type $\alpha$ and any finite sets $s$ and $t$ of elements of $\alpha$, the union of $s$ with the insertion of $a$ into $t$ is equal to the insertion of $a$ into the union of $s$ and $t$, i.e., $$ s \cup (t \cup \{a\}) = (s \cup t) \cup \{a\}. $$

Finset.insert_union_distrib theorem

(a : α) (s t : Finset α) : insert a (s ∪ t) = insert a s ∪ insert a t

Full source

theorem insert_union_distrib (a : α) (s t : Finset α) :
    insert a (s ∪ t) = insertinsert a s ∪ insert a t := by
  simp only [insert_union, union_insert, insert_idem]

Distributivity of Insertion over Union for Finite Sets

Informal description

For any element $a$ of type $\alpha$ and any finite sets $s$ and $t$ of elements of $\alpha$, the insertion of $a$ into the union of $s$ and $t$ is equal to the union of the insertion of $a$ into $s$ and the insertion of $a$ into $t$, i.e., $$ \{a\} \cup (s \cup t) = (\{a\} \cup s) \cup (\{a\} \cup t). $$

Finset.induction_on_union theorem

 (P : Finset α → Finset α → Prop) (symm : ∀ {a b}, P a b → P b a) (empty_right : ∀ {a}, P a ∅)
  (singletons : ∀ {a b}, P { a } { b }) (union_of : ∀ {a b c}, P a c → P b c → P (a ∪ b) c) : ∀ a b, P a b

Full source

/-- To prove a relation on pairs of `Finset X`, it suffices to show that it is
  * symmetric,
  * it holds when one of the `Finset`s is empty,
  * it holds for pairs of singletons,
  * if it holds for `[a, c]` and for `[b, c]`, then it holds for `[a ∪ b, c]`.
-/
theorem induction_on_union (P : Finset α → Finset α → Prop) (symm : ∀ {a b}, P a b → P b a)
    (empty_right : ∀ {a}, P a ∅) (singletons : ∀ {a b}, P {a} {b})
    (union_of : ∀ {a b c}, P a c → P b c → P (a ∪ b) c) : ∀ a b, P a b := by
  intro a b
  refine Finset.induction_on b empty_right fun x s _xs hi => symm ?_
  rw [Finset.insert_eq]
  apply union_of _ (symm hi)
  refine Finset.induction_on a empty_right fun a t _ta hi => symm ?_
  rw [Finset.insert_eq]
  exact union_of singletons (symm hi)

Induction Principle for Binary Relations on Finite Sets via Union

Informal description

Let $P$ be a binary relation on finite sets of type $\alpha$. To prove that $P$ holds for all pairs of finite sets, it suffices to show: 1. $P$ is symmetric, i.e., $P(a, b) \to P(b, a)$ for any finite sets $a, b$, 2. $P$ holds when the second argument is empty, i.e., $P(a, \emptyset)$ for any finite set $a$, 3. $P$ holds for all pairs of singletons, i.e., $P(\{x\}, \{y\})$ for any $x, y \in \alpha$, 4. If $P$ holds for $(a, c)$ and $(b, c)$, then it holds for $(a \cup b, c)$.

Finset.inter_empty theorem

(s : Finset α) : s ∩ ∅ = ∅

Full source

@[simp]
theorem inter_empty (s : Finset α) : s ∩ ∅ = ∅ :=
  ext fun _ => mem_inter.trans <| by simp

Intersection with Empty Set Yields Empty Set

Informal description

For any finite set $s$ of elements of type $\alpha$, the intersection of $s$ with the empty set is the empty set, i.e., $s \cap \emptyset = \emptyset$.

Finset.empty_inter theorem

(s : Finset α) : ∅ ∩ s = ∅

Full source

@[simp]
theorem empty_inter (s : Finset α) : ∅∅ ∩ s = ∅ :=
  ext fun _ => mem_inter.trans <| by simp

Empty Set Intersection Property: $\emptyset \cap s = \emptyset$

Informal description

For any finite set $s$ of elements of type $\alpha$, the intersection of the empty set with $s$ is the empty set, i.e., $\emptyset \cap s = \emptyset$.

Finset.insert_inter_of_mem theorem

{s₁ s₂ : Finset α} {a : α} (h : a ∈ s₂) : insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)

Full source

@[simp]
theorem insert_inter_of_mem {s₁ s₂ : Finset α} {a : α} (h : a ∈ s₂) :
    insertinsert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂) :=
  ext fun x => by
    have : x = a ∨ x ∈ s₂x = a ∨ x ∈ s₂ ↔ x ∈ s₂ := or_iff_right_of_imp <| by rintro rfl; exact h
    simp only [mem_inter, mem_insert, or_and_left, this]

Insertion-Intersection Property for Finite Sets

Informal description

For any finite sets $s_1, s_2$ of type $\alpha$ and any element $a \in \alpha$ such that $a \in s_2$, the intersection of the set obtained by inserting $a$ into $s_1$ with $s_2$ is equal to the set obtained by inserting $a$ into the intersection of $s_1$ and $s_2$. In symbols: $$ \text{insert } a \text{ } s_1 \cap s_2 = \text{insert } a \text{ } (s_1 \cap s_2) $$

Finset.inter_insert_of_mem theorem

{s₁ s₂ : Finset α} {a : α} (h : a ∈ s₁) : s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

Full source

@[simp]
theorem inter_insert_of_mem {s₁ s₂ : Finset α} {a : α} (h : a ∈ s₁) :
    s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂) := by rw [inter_comm, insert_inter_of_mem h, inter_comm]

Intersection with Inserted Element When in First Set: $s_1 \cap (s_2 \cup \{a\}) = \{a\} \cup (s_1 \cap s_2)$ if $a \in s_1$

Informal description

For any finite sets $s_1, s_2$ of elements of type $\alpha$ and any element $a \in \alpha$ such that $a \in s_1$, the intersection of $s_1$ with the set obtained by inserting $a$ into $s_2$ is equal to the set obtained by inserting $a$ into the intersection of $s_1$ and $s_2$. In symbols: $$ s_1 \cap (s_2 \cup \{a\}) = \{a\} \cup (s_1 \cap s_2) $$

Finset.insert_inter_of_not_mem theorem

{s₁ s₂ : Finset α} {a : α} (h : a ∉ s₂) : insert a s₁ ∩ s₂ = s₁ ∩ s₂

Full source

@[simp]
theorem insert_inter_of_not_mem {s₁ s₂ : Finset α} {a : α} (h : a ∉ s₂) :
    insertinsert a s₁ ∩ s₂ = s₁ ∩ s₂ :=
  ext fun x => by
    have : ¬(x = a ∧ x ∈ s₂) := by rintro ⟨rfl, H⟩; exact h H
    simp only [mem_inter, mem_insert, or_and_right, this, false_or]

Intersection with Inserted Element When Not in Second Set: $(s_1 \cup \{a\}) \cap s_2 = s_1 \cap s_2$ if $a \notin s_2$

Informal description

For any finite sets $s_1, s_2$ of type $\alpha$ and any element $a \in \alpha$ such that $a \notin s_2$, the intersection of $\{a\} \cup s_1$ with $s_2$ equals the intersection of $s_1$ with $s_2$, i.e., $(s_1 \cup \{a\}) \cap s_2 = s_1 \cap s_2$.

Finset.inter_insert_of_not_mem theorem

{s₁ s₂ : Finset α} {a : α} (h : a ∉ s₁) : s₁ ∩ insert a s₂ = s₁ ∩ s₂

Full source

@[simp]
theorem inter_insert_of_not_mem {s₁ s₂ : Finset α} {a : α} (h : a ∉ s₁) :
    s₁ ∩ insert a s₂ = s₁ ∩ s₂ := by rw [inter_comm, insert_inter_of_not_mem h, inter_comm]

Intersection with Inserted Element When Not in First Set: $s_1 \cap (s_2 \cup \{a\}) = s_1 \cap s_2$ if $a \notin s_1$

Informal description

For any finite sets $s_1, s_2$ of elements of type $\alpha$ and any element $a \in \alpha$ such that $a \notin s_1$, the intersection of $s_1$ with the set obtained by inserting $a$ into $s_2$ is equal to the intersection of $s_1$ with $s_2$, i.e., $s_1 \cap (s_2 \cup \{a\}) = s_1 \cap s_2$.

Finset.singleton_inter_of_mem theorem

{a : α} {s : Finset α} (H : a ∈ s) : { a } ∩ s = { a }

Full source

@[simp]
theorem singleton_inter_of_mem {a : α} {s : Finset α} (H : a ∈ s) : {a}{a} ∩ s = {a} :=
  show insertinsert a ∅ ∩ s = insert a ∅ by rw [insert_inter_of_mem H, empty_inter]

Intersection of Singleton with Finite Set When Element is Present: $\{a\} \cap s = \{a\}$ if $a \in s$

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, if $a$ belongs to $s$, then the intersection of the singleton set $\{a\}$ with $s$ is $\{a\}$, i.e., $\{a\} \cap s = \{a\}$.

Finset.singleton_inter_of_not_mem theorem

{a : α} {s : Finset α} (H : a ∉ s) : { a } ∩ s = ∅

Full source

@[simp]
theorem singleton_inter_of_not_mem {a : α} {s : Finset α} (H : a ∉ s) : {a}{a} ∩ s = ∅ :=
  eq_empty_of_forall_not_mem <| by
    simp only [mem_inter, mem_singleton]; rintro x ⟨rfl, h⟩; exact H h

Intersection of Singleton with Finite Set is Empty When Element Not in Set

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, if $a$ does not belong to $s$, then the intersection of the singleton set $\{a\}$ with $s$ is the empty set, i.e., $\{a\} \cap s = \emptyset$.

Finset.singleton_inter theorem

{a : α} {s : Finset α} : { a } ∩ s = if a ∈ s then { a } else ∅

Full source

lemma singleton_inter {a : α} {s : Finset α} :
    {a}{a} ∩ s = if a ∈ s then {a} else ∅ := by
  split_ifs with h <;> simp [h]

Intersection of Singleton with Finite Set: $\{a\} \cap s = \text{if } a \in s \text{ then } \{a\} \text{ else } \emptyset$

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, the intersection of the singleton set $\{a\}$ with $s$ is $\{a\}$ if $a \in s$, and the empty set otherwise. That is: $$\{a\} \cap s = \begin{cases} \{a\} & \text{if } a \in s, \\ \emptyset & \text{otherwise.} \end{cases}$$

Finset.inter_singleton_of_mem theorem

{a : α} {s : Finset α} (h : a ∈ s) : s ∩ { a } = { a }

Full source

@[simp]
theorem inter_singleton_of_mem {a : α} {s : Finset α} (h : a ∈ s) : s ∩ {a} = {a} := by
  rw [inter_comm, singleton_inter_of_mem h]

Intersection of Finite Set with Singleton When Element is Present: $s \cap \{a\} = \{a\}$ if $a \in s$

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, if $a$ belongs to $s$, then the intersection of $s$ with the singleton set $\{a\}$ is $\{a\}$, i.e., $s \cap \{a\} = \{a\}$.

Finset.inter_singleton_of_not_mem theorem

{a : α} {s : Finset α} (h : a ∉ s) : s ∩ { a } = ∅

Full source

@[simp]
theorem inter_singleton_of_not_mem {a : α} {s : Finset α} (h : a ∉ s) : s ∩ {a} = ∅ := by
  rw [inter_comm, singleton_inter_of_not_mem h]

Intersection of Finite Set with Singleton is Empty When Element Not in Set

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, if $a$ does not belong to $s$, then the intersection of $s$ with the singleton set $\{a\}$ is the empty set, i.e., $s \cap \{a\} = \emptyset$.

Finset.inter_singleton theorem

{a : α} {s : Finset α} : s ∩ { a } = if a ∈ s then { a } else ∅

Full source

lemma inter_singleton {a : α} {s : Finset α} :
    s ∩ {a} = if a ∈ s then {a} else ∅ := by
  split_ifs with h <;> simp [h]

Intersection of Finite Set with Singleton: $s \cap \{a\} = \{a\}$ if $a \in s$, $\emptyset$ otherwise

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, the intersection $s \cap \{a\}$ equals $\{a\}$ if $a \in s$, and equals $\emptyset$ otherwise.

Finset.union_eq_empty theorem

: s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

Full source

@[simp] lemma union_eq_empty : s ∪ ts ∪ t = ∅ ↔ s = ∅ ∧ t = ∅ := sup_eq_bot_iff

Union of Finite Sets is Empty iff Both Sets Are Empty

Informal description

For any finite sets $s$ and $t$ of elements of type $\alpha$, the union $s \cup t$ is empty if and only if both $s$ and $t$ are empty, i.e., $s \cup t = \emptyset \leftrightarrow s = \emptyset \land t = \emptyset$.

Finset.union_nonempty theorem

: (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty

Full source

@[simp] lemma union_nonempty : (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty :=
  mod_cast Set.union_nonempty (α := α) (s := s) (t := t)

Nonempty Union Characterization for Finite Sets: $s \cup t \neq \emptyset \leftrightarrow s \neq \emptyset \lor t \neq \emptyset$

Informal description

For any finite sets $s$ and $t$ of elements of type $\alpha$, the union $s \cup t$ is nonempty if and only if at least one of $s$ or $t$ is nonempty, i.e., $s \cup t \neq \emptyset \leftrightarrow s \neq \emptyset \lor t \neq \emptyset$.

Finset.insert_union_comm theorem

(s t : Finset α) (a : α) : insert a s ∪ t = s ∪ insert a t

Full source

theorem insert_union_comm (s t : Finset α) (a : α) : insertinsert a s ∪ t = s ∪ insert a t := by
  rw [insert_union, union_insert]

Commutativity of Insertion and Union for Finite Sets

Informal description

For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$, the union of the insertion of $a$ into $s$ with $t$ is equal to the union of $s$ with the insertion of $a$ into $t$, i.e., $$ (\{a\} \cup s) \cup t = s \cup (\{a\} \cup t). $$

List.toFinset_append theorem

: toFinset (l ++ l') = l.toFinset ∪ l'.toFinset

Full source

@[simp]
theorem toFinset_append : toFinset (l ++ l') = l.toFinset ∪ l'.toFinset := by
  induction' l with hd tl hl
  · simp
  · simp [hl]

Finite Set of Concatenated Lists Equals Union of Finite Sets

Informal description

For any two lists $l$ and $l'$ with elements of type $\alpha$, the finite set constructed from their concatenation $l \mathbin{+\!\!+} l'$ is equal to the union of the finite sets constructed from $l$ and $l'$ individually, i.e., $$ \text{toFinset}(l \mathbin{+\!\!+} l') = \text{toFinset}(l) \cup \text{toFinset}(l'). $$

Tags