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]
@[simp]
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]
@[simp]
@[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.insert_union_comm
{α : Type u_1}
[DecidableEq α]
(s t : Finset α)
(a : α)
:
insert a s ∪ t = s ∪ insert a t
@[simp]