Documentation

Mathlib.Data.Finset.Lattice.Basic

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.

Operations on two or more finsets #

Tags #

finite sets, finset

Lattice structure #

instance Finset.instUnion {α : Type u_1} [DecidableEq α] :

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

Equations
    instance Finset.instInter {α : Type u_1} [DecidableEq α] :

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

    Equations
      instance Finset.instLattice {α : Type u_1} [DecidableEq α] :
      Equations
        @[simp]
        @[simp]

        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} :
        (∀ as t, p a) (∀ as, p a) at, p a
        theorem Finset.notMem_union {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :
        as t as at
        @[deprecated Finset.notMem_union (since := "2025-05-23")]
        theorem Finset.not_mem_union {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :
        as t as at

        Alias of Finset.notMem_union.

        @[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 us 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
        @[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
        @[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
        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₁ us₁ 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
        Equations
          @[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)
          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'