HepLean Documentation

Mathlib.Data.Finset.Lattice.Lemmas

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 #

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

union #

source
@[simp]
theorem Finset.union_empty {α : Type u_1} [DecidableEq α] (s : Finset α) :
s ∪ ∅ = s
source
@[simp]
theorem Finset.empty_union {α : Type u_1} [DecidableEq α] (s : Finset α) :
∅ ∪ s = s
source
theorem Finset.Nonempty.inl {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s.Nonempty) :
(s ∪ t).Nonempty
source
theorem Finset.Nonempty.inr {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : t.Nonempty) :
(s ∪ t).Nonempty
source
theorem Finset.insert_eq {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
insert a s = {a} ∪ s
source
@[simp]
theorem Finset.insert_union {α : Type u_1} [DecidableEq α] (a : α) (s t : Finset α) :
insert a s ∪ t = insert a (s ∪ t)
source
@[simp]
theorem Finset.union_insert {α : Type u_1} [DecidableEq α] (a : α) (s t : Finset α) :
s ∪ insert a t = insert a (s ∪ t)
source
theorem Finset.insert_union_distrib {α : Type u_1} [DecidableEq α] (a : α) (s t : Finset α) :
insert a (s ∪ t) = insert a s ∪ insert a t
source
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 #

source
@[simp]
theorem Finset.inter_empty {α : Type u_1} [DecidableEq α] (s : Finset α) :
s ∩ ∅ = ∅
source
@[simp]
theorem Finset.empty_inter {α : Type u_1} [DecidableEq α] (s : Finset α) :
∅ ∩ s = ∅
source
@[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₂)
source
@[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₂)
source
@[simp]
theorem Finset.insert_inter_of_not_mem {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} {a : α} (h : a ∉ s₂) :
insert a s₁ ∩ s₂ = s₁ ∩ s₂
source
@[simp]
theorem Finset.inter_insert_of_not_mem {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} {a : α} (h : a ∉ s₁) :
s₁ ∩ insert a s₂ = s₁ ∩ s₂
source
@[simp]
theorem Finset.singleton_inter_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (H : a ∈ s) :
{a} ∩ s = {a}
source
@[simp]
theorem Finset.singleton_inter_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (H : a ∉ s) :
{a} ∩ s = ∅
source
theorem Finset.singleton_inter {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} :
{a} ∩ s = if a ∈ s then {a} else ∅
source
@[simp]
theorem Finset.inter_singleton_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∈ s) :
s ∩ {a} = {a}
source
@[simp]
theorem Finset.inter_singleton_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) :
s ∩ {a} = ∅
source
theorem Finset.inter_singleton {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} :
s ∩ {a} = if a ∈ s then {a} else ∅
source
theorem Finset.union_eq_empty {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅
source
theorem Finset.insert_union_comm {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) :
insert a s ∪ t = s ∪ insert a t
source
@[simp]
theorem List.toFinset_append {α : Type u_1} [DecidableEq α] {l l' : List α} :
(l ++ l').toFinset = l.toFinset ∪ l'.toFinset