Lemmas about the lattice structure of finite sets

This file contains many results on the lattice structure of Finset α, in particular the interaction between union, intersection, empty set and inserting elements.

Tags

finite sets, finset

Lattice structure

theorem Finset.disjoint_iff_inter_eq_empty {α : Type u_1} [DecidableEq α] {s t : Finset α} : Disjoint s t ↔ s ∩ t = ∅

union

@[simp]

theorem Finset.union_empty {α : Type u_1} [DecidableEq α] (s : Finset α) : s ∪ ∅ = s

@[simp]

theorem Finset.empty_union {α : Type u_1} [DecidableEq α] (s : Finset α) : ∅ ∪ s = s

theorem Finset.Nonempty.inl {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s.Nonempty) : (s ∪ t).Nonempty

theorem Finset.Nonempty.inr {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : t.Nonempty) : (s ∪ t).Nonempty

theorem Finset.insert_eq {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : insert a s = {a} ∪ s

@[simp]

theorem Finset.singleton_union {α : Type u_1} [DecidableEq α] (x : α) (s : Finset α) : {x} ∪ s = insert x s

@[simp]

theorem Finset.union_singleton {α : Type u_1} [DecidableEq α] (x : α) (s : Finset α) : s ∪ {x} = insert x s

@[simp]

theorem Finset.insert_union {α : Type u_1} [DecidableEq α] (a : α) (s t : Finset α) : insert a s ∪ t = insert a (s ∪ t)

@[simp]

theorem Finset.union_insert {α : Type u_1} [DecidableEq α] (a : α) (s t : Finset α) : s ∪ insert a t = insert a (s ∪ t)

theorem Finset.insert_union_distrib {α : Type u_1} [DecidableEq α] (a : α) (s t : Finset α) : insert a (s ∪ t) = insert a s ∪ insert a t

theorem Finset.induction_on_union {α : Type u_1} [DecidableEq α] (P : Finset α → Finset α → Prop) (symm : ∀ {a b : Finset α}, P a b → P b a) (empty_right : ∀ {a : Finset α}, P a ∅) (singletons : ∀ {a b : α}, P {a} {b}) (union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c) (a b : Finset α) : P a b

To prove a relation on pairs of Finset X, it suffices to show that it is

• symmetric,
• it holds when one of the Finsets 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].

inter

@[simp]

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

@[simp]

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

@[simp]

theorem Finset.insert_inter_of_mem {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} {a : α} (h : a ∈ s₂) : insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)

@[simp]

theorem Finset.inter_insert_of_mem {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} {a : α} (h : a ∈ s₁) : s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

@[simp]

theorem Finset.insert_inter_of_notMem {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} {a : α} (h : a ∉ s₂) : insert a s₁ ∩ s₂ = s₁ ∩ s₂

@[simp]

theorem Finset.inter_insert_of_notMem {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} {a : α} (h : a ∉ s₁) : s₁ ∩ insert a s₂ = s₁ ∩ s₂

theorem Finset.inter_insert {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} {a : α} : insert a s₁ ∩ s₂ = if a ∈ s₂ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

theorem Finset.insert_inter {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} {a : α} : s₁ ∩ insert a s₂ = if a ∈ s₁ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

@[simp]

theorem Finset.singleton_inter_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (H : a ∈ s) : {a} ∩ s = {a}

@[simp]

theorem Finset.singleton_inter_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (H : a ∉ s) : {a} ∩ s = ∅

theorem Finset.singleton_inter {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} : {a} ∩ s = if a ∈ s then {a} else ∅

@[simp]

theorem Finset.inter_singleton_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∈ s) : s ∩ {a} = {a}

@[simp]

theorem Finset.inter_singleton_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : s ∩ {a} = ∅

theorem Finset.inter_singleton {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} : s ∩ {a} = if a ∈ s then {a} else ∅

@[simp]

theorem Finset.union_eq_empty {α : Type u_1} [DecidableEq α] {s t : Finset α} : s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

@[simp]

theorem Finset.union_nonempty {α : Type u_1} [DecidableEq α] {s t : Finset α} : (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty

theorem Finset.insert_union_comm {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) : insert a s ∪ t = s ∪ insert a t

@[simp]

theorem List.toFinset_append {α : Type u_1} [DecidableEq α] {l l' : List α} : (l ++ l').toFinset = l.toFinset ∪ l'.toFinset