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"
• Finset.instSDiffFinset: Defines the set difference s \ t for finsets s and t.

Tags

finite sets, finset

Lattice structure

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 := ⋯ } }

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 := ⋯ } }

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

Equations

• Finset.instLattice = Lattice.mk (fun (x1 x2 : Finset α) => x1 ∩ x2) ⋯ ⋯ ⋯

@[simp]

theorem Finset.sup_eq_union {α : Type u_1} [DecidableEq α] : max = Union.union

@[simp]

theorem Finset.inf_eq_inter {α : Type u_1} [DecidableEq α] : min = Inter.inter

union

theorem Finset.union_val_nd {α : Type u_1} [DecidableEq α] (s t : Finset α) : (s ∪ t).val = s.val.ndunion t.val

@[simp]

theorem Finset.union_val {α : Type u_1} [DecidableEq α] (s t : Finset α) : (s ∪ t).val = s.val ∪ t.val

@[simp]

theorem Finset.mem_union {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} : a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t

theorem Finset.mem_union_left {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s) : a ∈ s ∪ t

theorem Finset.mem_union_right {α : Type u_1} [DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t) : a ∈ s ∪ t

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

theorem Finset.not_mem_union {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} : a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t

@[simp]

theorem Finset.coe_union {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : ↑(s₁ ∪ s₂) = ↑s₁ ∪ ↑s₂

theorem Finset.union_subset {α : Type u_1} [DecidableEq α] {s t u : Finset α} (hs : s ⊆ u) : t ⊆ u → s ∪ t ⊆ u

@[simp]

theorem Finset.subset_union_left {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} : s₁ ⊆ s₁ ∪ s₂

@[simp]

theorem Finset.subset_union_right {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} : s₂ ⊆ s₁ ∪ s₂

theorem Finset.union_subset_union {α : Type u_1} [DecidableEq α] {s t u v : Finset α} (hsu : s ⊆ u) (htv : t ⊆ v) : s ∪ t ⊆ u ∪ v

theorem Finset.union_subset_union_left {α : Type u_1} [DecidableEq α] {s₁ s₂ t : Finset α} (h : s₁ ⊆ s₂) : s₁ ∪ t ⊆ s₂ ∪ t

theorem Finset.union_subset_union_right {α : Type u_1} [DecidableEq α] {s t₁ t₂ : Finset α} (h : t₁ ⊆ t₂) : s ∪ t₁ ⊆ s ∪ t₂

theorem Finset.union_comm {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : s₁ ∪ s₂ = s₂ ∪ s₁

instance Finset.instCommutativeUnion {α : Type u_1} [DecidableEq α] : Std.Commutative fun (x1 x2 : Finset α) => x1 ∪ x2

Equations

• ⋯ = ⋯

@[simp]

theorem Finset.union_assoc {α : Type u_1} [DecidableEq α] (s₁ s₂ s₃ : Finset α) : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)

instance Finset.instAssociativeUnion {α : Type u_1} [DecidableEq α] : Std.Associative fun (x1 x2 : Finset α) => x1 ∪ x2

Equations

• ⋯ = ⋯

@[simp]

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

instance Finset.instIdempotentOpUnion {α : Type u_1} [DecidableEq α] : Std.IdempotentOp fun (x1 x2 : Finset α) => x1 ∪ x2

Equations

• ⋯ = ⋯

theorem Finset.union_subset_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} (h : s ∪ t ⊆ u) : s ⊆ u

theorem Finset.union_subset_right {α : Type u_1} [DecidableEq α] {s t u : Finset α} (h : s ∪ t ⊆ u) : t ⊆ u

theorem Finset.union_left_comm {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∪ (t ∪ u) = t ∪ (s ∪ u)

theorem Finset.union_right_comm {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∪ t ∪ u = s ∪ u ∪ t

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

@[simp]

theorem Finset.union_eq_left {α : Type u_1} [DecidableEq α] {s t : Finset α} : s ∪ t = s ↔ t ⊆ s

@[simp]

theorem Finset.left_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} : s = s ∪ t ↔ t ⊆ s

@[simp]

theorem Finset.union_eq_right {α : Type u_1} [DecidableEq α] {s t : Finset α} : s ∪ t = t ↔ s ⊆ t

@[simp]

theorem Finset.right_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} : s = t ∪ s ↔ t ⊆ s

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

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

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

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

theorem Finset.inter_val_nd {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : (s₁ ∩ s₂).val = s₁.val.ndinter s₂.val

@[simp]

theorem Finset.inter_val {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : (s₁ ∩ s₂).val = s₁.val ∩ s₂.val

@[simp]

theorem Finset.mem_inter {α : Type u_1} [DecidableEq α] {a : α} {s₁ s₂ : Finset α} : a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂

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

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

theorem Finset.mem_inter_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s₁ s₂ : Finset α} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂

@[simp]

theorem Finset.inter_subset_left {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} : s₁ ∩ s₂ ⊆ s₁

@[simp]

theorem Finset.inter_subset_right {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} : s₁ ∩ s₂ ⊆ s₂

theorem Finset.subset_inter {α : Type u_1} [DecidableEq α] {s₁ s₂ u : Finset α} : s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u

@[simp]

theorem Finset.coe_inter {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : ↑(s₁ ∩ s₂) = ↑s₁ ∩ ↑s₂

@[simp]

theorem Finset.union_inter_cancel_left {α : Type u_1} [DecidableEq α] {s t : Finset α} : (s ∪ t) ∩ s = s

@[simp]

theorem Finset.union_inter_cancel_right {α : Type u_1} [DecidableEq α] {s t : Finset α} : (s ∪ t) ∩ t = t

theorem Finset.inter_comm {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : s₁ ∩ s₂ = s₂ ∩ s₁

@[simp]

theorem Finset.inter_assoc {α : Type u_1} [DecidableEq α] (s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃)

theorem Finset.inter_left_comm {α : Type u_1} [DecidableEq α] (s₁ s₂ s₃ : Finset α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)

theorem Finset.inter_right_comm {α : Type u_1} [DecidableEq α] (s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂

@[simp]

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

@[simp]

theorem Finset.inter_union_self {α : Type u_1} [DecidableEq α] (s t : Finset α) : s ∩ (t ∪ s) = s

theorem Finset.inter_subset_inter {α : Type u_1} [DecidableEq α] {x y s t : Finset α} (h : x ⊆ y) (h' : s ⊆ t) : x ∩ s ⊆ y ∩ t

theorem Finset.inter_subset_inter_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} (h : t ⊆ u) : s ∩ t ⊆ s ∩ u

theorem Finset.inter_subset_inter_right {α : Type u_1} [DecidableEq α] {s t u : Finset α} (h : s ⊆ t) : s ∩ u ⊆ t ∩ u

theorem Finset.inter_subset_union {α : Type u_1} [DecidableEq α] {s t : Finset α} : s ∩ t ⊆ s ∪ t

instance Finset.instDistribLattice {α : Type u_1} [DecidableEq α] : DistribLattice (Finset α)

Equations

• Finset.instDistribLattice = DistribLattice.mk ⋯

@[simp]

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

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

@[simp]

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

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

theorem Finset.inter_union_distrib_left {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

theorem Finset.union_inter_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) : (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u

theorem Finset.union_inter_distrib_left {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

theorem Finset.inter_union_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)

@[deprecated Finset.inter_union_distrib_left]

theorem Finset.inter_distrib_left {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

Alias of Finset.inter_union_distrib_left.

@[deprecated Finset.union_inter_distrib_right]

theorem Finset.inter_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) : (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u

Alias of Finset.union_inter_distrib_right.

@[deprecated Finset.union_inter_distrib_left]

theorem Finset.union_distrib_left {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

Alias of Finset.union_inter_distrib_left.

@[deprecated Finset.inter_union_distrib_right]

theorem Finset.union_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)

Alias of Finset.inter_union_distrib_right.

theorem Finset.union_union_distrib_left {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)

theorem Finset.union_union_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)

theorem Finset.inter_inter_distrib_left {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)

theorem Finset.inter_inter_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)

theorem Finset.union_union_union_comm {α : Type u_1} [DecidableEq α] (s t u v : Finset α) : s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)

theorem Finset.inter_inter_inter_comm {α : Type u_1} [DecidableEq α] (s t u v : Finset α) : s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)

theorem Finset.union_subset_iff {α : Type u_1} [DecidableEq α] {s t u : Finset α} : s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u

theorem Finset.subset_inter_iff {α : Type u_1} [DecidableEq α] {s t u : Finset α} : s ⊆ t ∩ u ↔ s ⊆ t ∧ s ⊆ u

@[simp]

theorem Finset.inter_eq_left {α : Type u_1} [DecidableEq α] {s t : Finset α} : s ∩ t = s ↔ s ⊆ t

@[simp]

theorem Finset.inter_eq_right {α : Type u_1} [DecidableEq α] {s t : Finset α} : t ∩ s = s ↔ s ⊆ t

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

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

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

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

theorem Finset.ite_subset_union {α : Type u_1} [DecidableEq α] (s s' : Finset α) (P : Prop) [Decidable P] : (if P then s else s') ⊆ s ∪ s'

theorem Finset.inter_subset_ite {α : Type u_1} [DecidableEq α] (s s' : Finset α) (P : Prop) [Decidable P] : s ∩ s' ⊆ if P then s else s'