# Lattice structure on finite sets #

This file puts a lattice structure on finite sets using the union and intersection operators.

For `Finset α`, where `α` is a lattice, see also `Mathlib/Data/Finset/Lattice/Fold.lean`.

## Main declarations #

There is a natural lattice structure on the subsets of a set. In Lean, we use lattice notation to talk about things involving unions and intersections. See `Mathlib/Order/Lattice.lean`. For the lattice structure on finsets, `⊥` is called `bot` with `⊥ = ∅` and `⊤` is called `top` with `⊤ = univ`.

- `Finset.instHasSubsetFinset`: Lots of API about lattices, otherwise behaves as one would expect.
- `Finset.instUnionFinset`: Defines `s ∪ t` (or `s ⊔ t`) as the union of `s` and `t`. See `Finset.sup`/`Finset.biUnion` for finite unions.
- `Finset.instInterFinset`: Defines `s ∩ t` (or `s ⊓ t`) as the intersection of `s` and `t`. See `Finset.inf` for finite intersections.

### Operations on two or more finsets #

- `Finset.instUnionFinset`: see "The lattice structure on subsets of finsets"
- `Finset.instInterFinset`: see "The lattice structure on subsets of finsets"

## Tags #

finite sets, finset

### Lattice structure #

source
instance Finset.instUnion {α : Type u_1} [DecidableEq α] :
Union (Finset α)

`s ∪ t` is the set such that `a ∈ s ∪ t` iff `a ∈ s` or `a ∈ t`.

Equations

- Finset.instUnion = { union := fun (s t : Finset α) => { val := s.val.ndunion t.val, nodup := ⋯ } }

source
instance Finset.instInter {α : Type u_1} [DecidableEq α] :
Inter (Finset α)

`s ∩ t` is the set such that `a ∈ s ∩ t` iff `a ∈ s` and `a ∈ t`.

Equations

- Finset.instInter = { inter := fun (s t : Finset α) => { val := s.val.ndinter t.val, nodup := ⋯ } }

source
instance Finset.instLattice {α : Type u_1} [DecidableEq α] :
Lattice (Finset α)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem Finset.sup_eq_union' {α : Type u_1} [DecidableEq α] :
max = Union.union
source
theorem Finset.sup_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s ⊔ t = s ∪ t
source
@[simp]
theorem Finset.inf_eq_inter' {α : Type u_1} [DecidableEq α] :
min = Inter.inter
source
theorem Finset.inf_eq_inter {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s ⊓ t = s ∩ t

#### union #

source
theorem Finset.union_val_nd {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∪ t).val = s.val.ndunion t.val
source
@[simp]
theorem Finset.union_val {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∪ t).val = s.val ∪ t.val
source
@[simp]
theorem Finset.mem_union {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :
a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
source
theorem Finset.mem_union_left {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s) :
a ∈ s ∪ t
source
theorem Finset.mem_union_right {α : Type u_1} [DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t) :
a ∈ s ∪ t
source
theorem Finset.forall_mem_union {α : Type u_1} [DecidableEq α] {s t : Finset α} {p : α → Prop} :
(∀ a ∈ s ∪ t, p a) ↔ (∀ a ∈ s, p a) ∧ ∀ a ∈ t, p a
source
theorem Finset.notMem_union {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :
a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t
source
@[deprecated Finset.notMem_union (since := "2025-05-23")]
theorem Finset.not_mem_union {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :
a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t

Alias of `Finset.notMem_union`.

source
@[simp]
theorem Finset.coe_union {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
↑(s₁ ∪ s₂) = ↑s₁ ∪ ↑s₂
source
theorem Finset.union_subset {α : Type u_1} [DecidableEq α] {s t u : Finset α} (hs : s ⊆ u) :
t ⊆ u → s ∪ t ⊆ u
source
@[simp]
theorem Finset.subset_union_left {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} :
s₁ ⊆ s₁ ∪ s₂
source
@[simp]
theorem Finset.subset_union_right {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} :
s₂ ⊆ s₁ ∪ s₂
source
theorem Finset.union_subset_union {α : Type u_1} [DecidableEq α] {s t u v : Finset α} (hsu : s ⊆ u) (htv : t ⊆ v) :
s ∪ t ⊆ u ∪ v
source
theorem Finset.union_subset_union_left {α : Type u_1} [DecidableEq α] {s₁ s₂ t : Finset α} (h : s₁ ⊆ s₂) :
s₁ ∪ t ⊆ s₂ ∪ t
source
theorem Finset.union_subset_union_right {α : Type u_1} [DecidableEq α] {s t₁ t₂ : Finset α} (h : t₁ ⊆ t₂) :
s ∪ t₁ ⊆ s ∪ t₂
source
theorem Finset.union_comm {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
s₁ ∪ s₂ = s₂ ∪ s₁
source
instance Finset.instCommutativeUnion {α : Type u_1} [DecidableEq α] :
Std.Commutative fun (x1 x2 : Finset α) => x1 ∪ x2
source
@[simp]
theorem Finset.union_assoc {α : Type u_1} [DecidableEq α] (s₁ s₂ s₃ : Finset α) :
s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)
source
instance Finset.instAssociativeUnion {α : Type u_1} [DecidableEq α] :
Std.Associative fun (x1 x2 : Finset α) => x1 ∪ x2
source
@[simp]
theorem Finset.union_idempotent {α : Type u_1} [DecidableEq α] (s : Finset α) :
s ∪ s = s
source
instance Finset.instIdempotentOpUnion {α : Type u_1} [DecidableEq α] :
Std.IdempotentOp fun (x1 x2 : Finset α) => x1 ∪ x2
source
theorem Finset.union_subset_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} (h : s ∪ t ⊆ u) :
s ⊆ u
source
theorem Finset.union_subset_right {α : Type u_1} [DecidableEq α] {s t u : Finset α} (h : s ∪ t ⊆ u) :
t ⊆ u
source
theorem Finset.union_left_comm {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s ∪ (t ∪ u) = t ∪ (s ∪ u)
source
theorem Finset.union_right_comm {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s ∪ t ∪ u = s ∪ u ∪ t
source
theorem Finset.union_self {α : Type u_1} [DecidableEq α] (s : Finset α) :
s ∪ s = s
source
@[simp]
theorem Finset.union_eq_left {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s ∪ t = s ↔ t ⊆ s
source
@[simp]
theorem Finset.left_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s = s ∪ t ↔ t ⊆ s
source
@[simp]
theorem Finset.union_eq_right {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s ∪ t = t ↔ s ⊆ t
source
@[simp]
theorem Finset.right_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s = t ∪ s ↔ t ⊆ s
source
theorem Finset.union_congr_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} (ht : t ⊆ s ∪ u) (hu : u ⊆ s ∪ t) :
s ∪ t = s ∪ u
source
theorem Finset.union_congr_right {α : Type u_1} [DecidableEq α] {s t u : Finset α} (hs : s ⊆ t ∪ u) (ht : t ⊆ s ∪ u) :
s ∪ u = t ∪ u
source
theorem Finset.union_eq_union_iff_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} :
s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t
source
theorem Finset.union_eq_union_iff_right {α : Type u_1} [DecidableEq α] {s t u : Finset α} :
s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u
source
theorem Finset.inter_val_nd {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
(s₁ ∩ s₂).val = s₁.val.ndinter s₂.val
source
@[simp]
theorem Finset.inter_val {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
(s₁ ∩ s₂).val = s₁.val ∩ s₂.val
source
@[simp]
theorem Finset.mem_inter {α : Type u_1} [DecidableEq α] {a : α} {s₁ s₂ : Finset α} :
a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂
source
theorem Finset.mem_of_mem_inter_left {α : Type u_1} [DecidableEq α] {a : α} {s₁ s₂ : Finset α} (h : a ∈ s₁ ∩ s₂) :
a ∈ s₁
source
theorem Finset.mem_of_mem_inter_right {α : Type u_1} [DecidableEq α] {a : α} {s₁ s₂ : Finset α} (h : a ∈ s₁ ∩ s₂) :
a ∈ s₂
source
theorem Finset.mem_inter_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s₁ s₂ : Finset α} :
a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂
source
@[simp]
theorem Finset.inter_subset_left {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} :
s₁ ∩ s₂ ⊆ s₁
source
@[simp]
theorem Finset.inter_subset_right {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} :
s₁ ∩ s₂ ⊆ s₂
source
theorem Finset.subset_inter {α : Type u_1} [DecidableEq α] {s₁ s₂ u : Finset α} :
s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u
source
@[simp]
theorem Finset.coe_inter {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
↑(s₁ ∩ s₂) = ↑s₁ ∩ ↑s₂
source
@[simp]
theorem Finset.union_inter_cancel_left {α : Type u_1} [DecidableEq α] {s t : Finset α} :
(s ∪ t) ∩ s = s
source
@[simp]
theorem Finset.union_inter_cancel_right {α : Type u_1} [DecidableEq α] {s t : Finset α} :
(s ∪ t) ∩ t = t
source
theorem Finset.inter_comm {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
s₁ ∩ s₂ = s₂ ∩ s₁
source
@[simp]
theorem Finset.inter_assoc {α : Type u_1} [DecidableEq α] (s₁ s₂ s₃ : Finset α) :
s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃)
source
theorem Finset.inter_left_comm {α : Type u_1} [DecidableEq α] (s₁ s₂ s₃ : Finset α) :
s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)
source
theorem Finset.inter_right_comm {α : Type u_1} [DecidableEq α] (s₁ s₂ s₃ : Finset α) :
s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂
source
@[simp]
theorem Finset.inter_self {α : Type u_1} [DecidableEq α] (s : Finset α) :
s ∩ s = s
source
@[simp]
theorem Finset.inter_union_self {α : Type u_1} [DecidableEq α] (s t : Finset α) :
s ∩ (t ∪ s) = s
source
theorem Finset.inter_subset_inter {α : Type u_1} [DecidableEq α] {x y s t : Finset α} (h : x ⊆ y) (h' : s ⊆ t) :
x ∩ s ⊆ y ∩ t
source
theorem Finset.inter_subset_inter_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} (h : t ⊆ u) :
s ∩ t ⊆ s ∩ u
source
theorem Finset.inter_subset_inter_right {α : Type u_1} [DecidableEq α] {s t u : Finset α} (h : s ⊆ t) :
s ∩ u ⊆ t ∩ u
source
theorem Finset.inter_subset_union {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s ∩ t ⊆ s ∪ t
source
instance Finset.instDistribLattice {α : Type u_1} [DecidableEq α] :
DistribLattice (Finset α)
Equations

- Finset.instDistribLattice = { toLattice := Finset.instLattice, le_sup_inf := ⋯ }

source
@[simp]
theorem Finset.union_left_idem {α : Type u_1} [DecidableEq α] (s t : Finset α) :
s ∪ (s ∪ t) = s ∪ t
source
theorem Finset.union_right_idem {α : Type u_1} [DecidableEq α] (s t : Finset α) :
s ∪ t ∪ t = s ∪ t
source
@[simp]
theorem Finset.inter_left_idem {α : Type u_1} [DecidableEq α] (s t : Finset α) :
s ∩ (s ∩ t) = s ∩ t
source
theorem Finset.inter_right_idem {α : Type u_1} [DecidableEq α] (s t : Finset α) :
s ∩ t ∩ t = s ∩ t
source
theorem Finset.inter_union_distrib_left {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u
source
theorem Finset.union_inter_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
(s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
source
theorem Finset.union_inter_distrib_left {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)
source
theorem Finset.inter_union_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)
source
theorem Finset.union_union_distrib_left {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)
source
theorem Finset.union_union_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)
source
theorem Finset.inter_inter_distrib_left {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)
source
theorem Finset.inter_inter_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)
source
theorem Finset.union_union_union_comm {α : Type u_1} [DecidableEq α] (s t u v : Finset α) :
s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)
source
theorem Finset.inter_inter_inter_comm {α : Type u_1} [DecidableEq α] (s t u v : Finset α) :
s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)
source
theorem Finset.union_subset_iff {α : Type u_1} [DecidableEq α] {s t u : Finset α} :
s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u
source
theorem Finset.subset_inter_iff {α : Type u_1} [DecidableEq α] {s t u : Finset α} :
s ⊆ t ∩ u ↔ s ⊆ t ∧ s ⊆ u
source
@[simp]
theorem Finset.inter_eq_left {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s ∩ t = s ↔ s ⊆ t
source
@[simp]
theorem Finset.inter_eq_right {α : Type u_1} [DecidableEq α] {s t : Finset α} :
t ∩ s = s ↔ s ⊆ t
source
theorem Finset.inter_congr_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} (ht : s ∩ u ⊆ t) (hu : s ∩ t ⊆ u) :
s ∩ t = s ∩ u
source
theorem Finset.inter_congr_right {α : Type u_1} [DecidableEq α] {s t u : Finset α} (hs : t ∩ u ⊆ s) (ht : s ∩ u ⊆ t) :
s ∩ u = t ∩ u
source
theorem Finset.inter_eq_inter_iff_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} :
s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u
source
theorem Finset.inter_eq_inter_iff_right {α : Type u_1} [DecidableEq α] {s t u : Finset α} :
s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t
source
theorem Finset.ite_subset_union {α : Type u_1} [DecidableEq α] (s s' : Finset α) (P : Prop) [Decidable P] :
(if P then s else s') ⊆ s ∪ s'
source
theorem Finset.inter_subset_ite {α : Type u_1} [DecidableEq α] (s s' : Finset α) (P : Prop) [Decidable P] :
s ∩ s' ⊆ if P then s else s'