Documentation

Mathlib.Data.Finset.Basic

Finite sets #

Terms of type Finset α are one way of talking about finite subsets of α in mathlib. Below, Finset α is defined as a structure with 2 fields:

  1. val is a Multiset α of elements;
  2. nodup is a proof that val has no duplicates.

Finsets in Lean are constructive in that they have an underlying List that enumerates their elements. In particular, any function that uses the data of the underlying list cannot depend on its ordering. This is handled on the Multiset level by multiset API, so in most cases one needn't worry about it explicitly.

Finsets give a basic foundation for defining finite sums and products over types:

  1. ∑ i in (s : Finset α), f i;
  2. ∏ i in (s : Finset α), f i.

Lean refers to these operations as big operators. More information can be found in Mathlib.Algebra.BigOperators.Basic.

Finsets are directly used to define fintypes in Lean. A Fintype α instance for a type α consists of a universal Finset α containing every term of α, called univ. See Mathlib.Data.Fintype.Basic. There is also univ', the noncomputable partner to univ, which is defined to be α as a finset if α is finite, and the empty finset otherwise. See Mathlib.Data.Fintype.Basic.

Finset.card, the size of a finset is defined in Mathlib.Data.Finset.Card. This is then used to define Fintype.card, the size of a type.

Main declarations #

Main definitions #

Finset constructions #

Finsets from functions #

The lattice structure on subsets of finsets #

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. For the lattice structure on finsets, is called bot with ⊥ = ∅ and is called top with ⊤ = univ.

Operations on two or more finsets #

Maps constructed using finsets #

Predicates on finsets #

Equivalences between finsets #

Tags #

finite sets, finset

structure Finset (α : Type u_4) :
Type u_4

Finset α is the type of finite sets of elements of α. It is implemented as a multiset (a list up to permutation) which has no duplicate elements.

Instances For
    instance Multiset.canLiftFinset {α : Type u_4} :
    CanLift (Multiset α) (Finset α) Finset.val Multiset.Nodup
    Equations
    • =
    theorem Finset.eq_of_veq {α : Type u_1} {s : Finset α} {t : Finset α} :
    s.val = t.vals = t
    theorem Finset.val_injective {α : Type u_1} :
    @[simp]
    theorem Finset.val_inj {α : Type u_1} {s : Finset α} {t : Finset α} :
    s.val = t.val s = t
    @[simp]
    theorem Finset.dedup_eq_self {α : Type u_1} [DecidableEq α] (s : Finset α) :
    Multiset.dedup s.val = s.val
    instance Finset.decidableEq {α : Type u_1} [DecidableEq α] :
    Equations

    membership #

    instance Finset.instMembershipFinset {α : Type u_1} :
    Equations
    • Finset.instMembershipFinset = { mem := fun (a : α) (s : Finset α) => a s.val }
    theorem Finset.mem_def {α : Type u_1} {a : α} {s : Finset α} :
    a s a s.val
    @[simp]
    theorem Finset.mem_val {α : Type u_1} {a : α} {s : Finset α} :
    a s.val a s
    @[simp]
    theorem Finset.mem_mk {α : Type u_1} {a : α} {s : Multiset α} {nd : Multiset.Nodup s} :
    a { val := s, nodup := nd } a s
    instance Finset.decidableMem {α : Type u_1} [_h : DecidableEq α] (a : α) (s : Finset α) :
    Equations
    @[simp]
    theorem Finset.forall_mem_not_eq {α : Type u_1} {s : Finset α} {a : α} :
    (bs, ¬a = b) as
    @[simp]
    theorem Finset.forall_mem_not_eq' {α : Type u_1} {s : Finset α} {a : α} :
    (bs, ¬b = a) as

    set coercion #

    def Finset.toSet {α : Type u_1} (s : Finset α) :
    Set α

    Convert a finset to a set in the natural way.

    Equations
    • s = {a : α | a s}
    Instances For
      instance Finset.instCoeTCFinsetSet {α : Type u_1} :
      CoeTC (Finset α) (Set α)

      Convert a finset to a set in the natural way.

      Equations
      • Finset.instCoeTCFinsetSet = { coe := Finset.toSet }
      @[simp]
      theorem Finset.mem_coe {α : Type u_1} {a : α} {s : Finset α} :
      a s a s
      @[simp]
      theorem Finset.setOf_mem {α : Type u_4} {s : Finset α} :
      {a : α | a s} = s
      @[simp]
      theorem Finset.coe_mem {α : Type u_1} {s : Finset α} (x : s) :
      x s
      theorem Finset.mk_coe {α : Type u_1} {s : Finset α} (x : s) {h : x s} :
      { val := x, property := h } = x
      instance Finset.decidableMem' {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
      Decidable (a s)
      Equations

      extensionality #

      theorem Finset.ext_iff {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      s₁ = s₂ ∀ (a : α), a s₁ a s₂
      theorem Finset.ext {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      (∀ (a : α), a s₁ a s₂)s₁ = s₂
      @[simp]
      theorem Finset.coe_inj {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      s₁ = s₂ s₁ = s₂
      theorem Finset.coe_injective {α : Type u_4} :
      Function.Injective Finset.toSet

      type coercion #

      Coercion from a finset to the corresponding subtype.

      Equations
      • Finset.instCoeSortFinsetType = { coe := fun (s : Finset α) => { x : α // x s } }
      theorem Finset.forall_coe {α : Type u_4} (s : Finset α) (p : { x : α // x s }Prop) :
      (∀ (x : { x : α // x s }), p x) ∀ (x : α) (h : x s), p { val := x, property := h }
      theorem Finset.exists_coe {α : Type u_4} (s : Finset α) (p : { x : α // x s }Prop) :
      (∃ (x : { x : α // x s }), p x) ∃ (x : α) (h : x s), p { val := x, property := h }
      instance Finset.PiFinsetCoe.canLift (ι : Type u_4) (α : ιType u_5) [_ne : ∀ (i : ι), Nonempty (α i)] (s : Finset ι) :
      CanLift ((i : { x : ι // x s }) → α i) ((i : ι) → α i) (fun (f : (i : ι) → α i) (i : { x : ι // x s }) => f i) fun (x : (i : { x : ι // x s }) → α i) => True
      Equations
      • =
      instance Finset.PiFinsetCoe.canLift' (ι : Type u_4) (α : Type u_5) [_ne : Nonempty α] (s : Finset ι) :
      CanLift ({ x : ι // x s }α) (ια) (fun (f : ια) (i : { x : ι // x s }) => f i) fun (x : { x : ι // x s }α) => True
      Equations
      • =
      instance Finset.FinsetCoe.canLift {α : Type u_1} (s : Finset α) :
      CanLift α { x : α // x s } Subtype.val fun (a : α) => a s
      Equations
      • =
      @[simp]
      theorem Finset.coe_sort_coe {α : Type u_1} (s : Finset α) :
      s = { x : α // x s }

      Subset and strict subset relations #

      Equations
      • Finset.instHasSubsetFinset = { Subset := fun (s t : Finset α) => ∀ ⦃a : α⦄, a sa t }
      Equations
      • Finset.instHasSSubsetFinset = { SSubset := fun (s t : Finset α) => s t ¬t s }
      instance Finset.partialOrder {α : Type u_1} :
      Equations
      instance Finset.instIsReflFinsetSubsetInstHasSubsetFinset {α : Type u_1} :
      IsRefl (Finset α) fun (x x_1 : Finset α) => x x_1
      Equations
      • =
      instance Finset.instIsTransFinsetSubsetInstHasSubsetFinset {α : Type u_1} :
      IsTrans (Finset α) fun (x x_1 : Finset α) => x x_1
      Equations
      • =
      instance Finset.instIsAntisymmFinsetSubsetInstHasSubsetFinset {α : Type u_1} :
      IsAntisymm (Finset α) fun (x x_1 : Finset α) => x x_1
      Equations
      • =
      instance Finset.instIsIrreflFinsetSSubsetInstHasSSubsetFinset {α : Type u_1} :
      IsIrrefl (Finset α) fun (x x_1 : Finset α) => x x_1
      Equations
      • =
      instance Finset.instIsTransFinsetSSubsetInstHasSSubsetFinset {α : Type u_1} :
      IsTrans (Finset α) fun (x x_1 : Finset α) => x x_1
      Equations
      • =
      instance Finset.instIsAsymmFinsetSSubsetInstHasSSubsetFinset {α : Type u_1} :
      IsAsymm (Finset α) fun (x x_1 : Finset α) => x x_1
      Equations
      • =
      Equations
      • =
      theorem Finset.subset_def {α : Type u_1} {s : Finset α} {t : Finset α} :
      s t s.val t.val
      theorem Finset.ssubset_def {α : Type u_1} {s : Finset α} {t : Finset α} :
      s t s t ¬t s
      @[simp]
      theorem Finset.Subset.refl {α : Type u_1} (s : Finset α) :
      s s
      theorem Finset.Subset.rfl {α : Type u_1} {s : Finset α} :
      s s
      theorem Finset.subset_of_eq {α : Type u_1} {s : Finset α} {t : Finset α} (h : s = t) :
      s t
      theorem Finset.Subset.trans {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} {s₃ : Finset α} :
      s₁ s₂s₂ s₃s₁ s₃
      theorem Finset.Superset.trans {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} {s₃ : Finset α} :
      s₁ s₂s₂ s₃s₁ s₃
      theorem Finset.mem_of_subset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} {a : α} :
      s₁ s₂a s₁a s₂
      theorem Finset.not_mem_mono {α : Type u_1} {s : Finset α} {t : Finset α} (h : s t) {a : α} :
      atas
      theorem Finset.Subset.antisymm {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} (H₁ : s₁ s₂) (H₂ : s₂ s₁) :
      s₁ = s₂
      theorem Finset.subset_iff {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      s₁ s₂ ∀ ⦃x : α⦄, x s₁x s₂
      @[simp]
      theorem Finset.coe_subset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      s₁ s₂ s₁ s₂
      @[simp]
      theorem Finset.val_le_iff {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      s₁.val s₂.val s₁ s₂
      theorem Finset.Subset.antisymm_iff {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      s₁ = s₂ s₁ s₂ s₂ s₁
      theorem Finset.not_subset {α : Type u_1} {s : Finset α} {t : Finset α} :
      ¬s t ∃ x ∈ s, xt
      @[simp]
      theorem Finset.le_eq_subset {α : Type u_1} :
      (fun (x x_1 : Finset α) => x x_1) = fun (x x_1 : Finset α) => x x_1
      @[simp]
      theorem Finset.lt_eq_subset {α : Type u_1} :
      (fun (x x_1 : Finset α) => x < x_1) = fun (x x_1 : Finset α) => x x_1
      theorem Finset.le_iff_subset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      s₁ s₂ s₁ s₂
      theorem Finset.lt_iff_ssubset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      s₁ < s₂ s₁ s₂
      @[simp]
      theorem Finset.coe_ssubset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      s₁ s₂ s₁ s₂
      @[simp]
      theorem Finset.val_lt_iff {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} :
      s₁.val < s₂.val s₁ s₂
      theorem Finset.val_strictMono {α : Type u_1} :
      StrictMono Finset.val
      theorem Finset.ssubset_iff_subset_ne {α : Type u_1} {s : Finset α} {t : Finset α} :
      s t s t s t
      theorem Finset.ssubset_iff_of_subset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} (h : s₁ s₂) :
      s₁ s₂ ∃ x ∈ s₂, xs₁
      theorem Finset.ssubset_of_ssubset_of_subset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} {s₃ : Finset α} (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
      s₁ s₃
      theorem Finset.ssubset_of_subset_of_ssubset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} {s₃ : Finset α} (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
      s₁ s₃
      theorem Finset.exists_of_ssubset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} (h : s₁ s₂) :
      ∃ x ∈ s₂, xs₁
      instance Finset.isWellFounded_ssubset {α : Type u_1} :
      IsWellFounded (Finset α) fun (x x_1 : Finset α) => x x_1
      Equations
      • =
      instance Finset.wellFoundedLT {α : Type u_1} :
      Equations
      • =

      Order embedding from Finset α to Set α #

      def Finset.coeEmb {α : Type u_1} :

      Coercion to Set α as an OrderEmbedding.

      Equations
      • Finset.coeEmb = { toEmbedding := { toFun := Finset.toSet, inj' := }, map_rel_iff' := }
      Instances For
        @[simp]
        theorem Finset.coe_coeEmb {α : Type u_1} :
        Finset.coeEmb = Finset.toSet

        Nonempty #

        def Finset.Nonempty {α : Type u_1} (s : Finset α) :

        The property s.Nonempty expresses the fact that the finset s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

        Equations
        • s.Nonempty = ∃ (x : α), x s
        Instances For
          instance Finset.decidableNonempty {α : Type u_1} {s : Finset α} :
          Decidable s.Nonempty
          Equations
          @[simp]
          theorem Finset.coe_nonempty {α : Type u_1} {s : Finset α} :
          Set.Nonempty s s.Nonempty
          theorem Finset.nonempty_coe_sort {α : Type u_1} {s : Finset α} :
          Nonempty { x : α // x s } s.Nonempty
          theorem Finset.Nonempty.to_set {α : Type u_1} {s : Finset α} :
          s.NonemptySet.Nonempty s

          Alias of the reverse direction of Finset.coe_nonempty.

          theorem Finset.Nonempty.coe_sort {α : Type u_1} {s : Finset α} :
          s.NonemptyNonempty { x : α // x s }

          Alias of the reverse direction of Finset.nonempty_coe_sort.

          theorem Finset.Nonempty.bex {α : Type u_1} {s : Finset α} (h : s.Nonempty) :
          ∃ (x : α), x s
          theorem Finset.Nonempty.mono {α : Type u_1} {s : Finset α} {t : Finset α} (hst : s t) (hs : s.Nonempty) :
          t.Nonempty
          theorem Finset.Nonempty.forall_const {α : Type u_1} {s : Finset α} (h : s.Nonempty) {p : Prop} :
          (xs, p) p
          theorem Finset.Nonempty.to_subtype {α : Type u_1} {s : Finset α} :
          s.NonemptyNonempty { x : α // x s }
          theorem Finset.Nonempty.to_type {α : Type u_1} {s : Finset α} :
          s.NonemptyNonempty α

          empty #

          def Finset.empty {α : Type u_1} :

          The empty finset

          Equations
          • Finset.empty = { val := 0, nodup := }
          Instances For
            Equations
            • Finset.instEmptyCollectionFinset = { emptyCollection := Finset.empty }
            instance Finset.inhabitedFinset {α : Type u_1} :
            Equations
            • Finset.inhabitedFinset = { default := }
            @[simp]
            theorem Finset.empty_val {α : Type u_1} :
            .val = 0
            @[simp]
            theorem Finset.not_mem_empty {α : Type u_1} (a : α) :
            a
            @[simp]
            theorem Finset.not_nonempty_empty {α : Type u_1} :
            ¬.Nonempty
            @[simp]
            theorem Finset.mk_zero {α : Type u_1} :
            { val := 0, nodup := } =
            theorem Finset.ne_empty_of_mem {α : Type u_1} {a : α} {s : Finset α} (h : a s) :
            theorem Finset.Nonempty.ne_empty {α : Type u_1} {s : Finset α} (h : s.Nonempty) :
            @[simp]
            theorem Finset.empty_subset {α : Type u_1} (s : Finset α) :
            theorem Finset.eq_empty_of_forall_not_mem {α : Type u_1} {s : Finset α} (H : ∀ (x : α), xs) :
            s =
            theorem Finset.eq_empty_iff_forall_not_mem {α : Type u_1} {s : Finset α} :
            s = ∀ (x : α), xs
            @[simp]
            theorem Finset.val_eq_zero {α : Type u_1} {s : Finset α} :
            s.val = 0 s =
            theorem Finset.subset_empty {α : Type u_1} {s : Finset α} :
            @[simp]
            theorem Finset.not_ssubset_empty {α : Type u_1} (s : Finset α) :
            theorem Finset.nonempty_of_ne_empty {α : Type u_1} {s : Finset α} (h : s ) :
            s.Nonempty
            theorem Finset.nonempty_iff_ne_empty {α : Type u_1} {s : Finset α} :
            s.Nonempty s
            @[simp]
            theorem Finset.not_nonempty_iff_eq_empty {α : Type u_1} {s : Finset α} :
            ¬s.Nonempty s =
            theorem Finset.eq_empty_or_nonempty {α : Type u_1} (s : Finset α) :
            s = s.Nonempty
            @[simp]
            theorem Finset.coe_empty {α : Type u_1} :
            =
            @[simp]
            theorem Finset.coe_eq_empty {α : Type u_1} {s : Finset α} :
            s = s =
            theorem Finset.isEmpty_coe_sort {α : Type u_1} {s : Finset α} :
            IsEmpty { x : α // x s } s =
            instance Finset.instIsEmpty {α : Type u_1} :
            IsEmpty { x : α // x }
            Equations
            • =
            theorem Finset.eq_empty_of_isEmpty {α : Type u_1} [IsEmpty α] (s : Finset α) :
            s =

            A Finset for an empty type is empty.

            Equations
            • Finset.instOrderBotFinsetToLEToPreorderPartialOrder = OrderBot.mk
            @[simp]
            theorem Finset.bot_eq_empty {α : Type u_1} :
            @[simp]
            theorem Finset.empty_ssubset {α : Type u_1} {s : Finset α} :
            s s.Nonempty
            theorem Finset.Nonempty.empty_ssubset {α : Type u_1} {s : Finset α} :
            s.Nonempty s

            Alias of the reverse direction of Finset.empty_ssubset.

            singleton #

            instance Finset.instSingletonFinset {α : Type u_1} :

            {a} : Finset a is the set {a} containing a and nothing else.

            This differs from insert a ∅ in that it does not require a DecidableEq instance for α.

            Equations
            • Finset.instSingletonFinset = { singleton := fun (a : α) => { val := {a}, nodup := } }
            @[simp]
            theorem Finset.singleton_val {α : Type u_1} (a : α) :
            {a}.val = {a}
            @[simp]
            theorem Finset.mem_singleton {α : Type u_1} {a : α} {b : α} :
            b {a} b = a
            theorem Finset.eq_of_mem_singleton {α : Type u_1} {x : α} {y : α} (h : x {y}) :
            x = y
            theorem Finset.not_mem_singleton {α : Type u_1} {a : α} {b : α} :
            a{b} a b
            theorem Finset.mem_singleton_self {α : Type u_1} (a : α) :
            a {a}
            @[simp]
            theorem Finset.val_eq_singleton_iff {α : Type u_1} {a : α} {s : Finset α} :
            s.val = {a} s = {a}
            @[simp]
            theorem Finset.singleton_inj {α : Type u_1} {a : α} {b : α} :
            {a} = {b} a = b
            @[simp]
            theorem Finset.singleton_nonempty {α : Type u_1} (a : α) :
            {a}.Nonempty
            @[simp]
            theorem Finset.singleton_ne_empty {α : Type u_1} (a : α) :
            {a}
            theorem Finset.empty_ssubset_singleton {α : Type u_1} {a : α} :
            {a}
            @[simp]
            theorem Finset.coe_singleton {α : Type u_1} (a : α) :
            {a} = {a}
            @[simp]
            theorem Finset.coe_eq_singleton {α : Type u_1} {s : Finset α} {a : α} :
            s = {a} s = {a}
            theorem Finset.coe_subset_singleton {α : Type u_1} {s : Finset α} {a : α} :
            s {a} s {a}
            theorem Finset.singleton_subset_coe {α : Type u_1} {s : Finset α} {a : α} :
            {a} s {a} s
            theorem Finset.eq_singleton_iff_unique_mem {α : Type u_1} {s : Finset α} {a : α} :
            s = {a} a s xs, x = a
            theorem Finset.eq_singleton_iff_nonempty_unique_mem {α : Type u_1} {s : Finset α} {a : α} :
            s = {a} s.Nonempty xs, x = a
            theorem Finset.nonempty_iff_eq_singleton_default {α : Type u_1} [Unique α] {s : Finset α} :
            s.Nonempty s = {default}
            theorem Finset.Nonempty.eq_singleton_default {α : Type u_1} [Unique α] {s : Finset α} :
            s.Nonemptys = {default}

            Alias of the forward direction of Finset.nonempty_iff_eq_singleton_default.

            theorem Finset.singleton_iff_unique_mem {α : Type u_1} (s : Finset α) :
            (∃ (a : α), s = {a}) ∃! (a : α), a s
            theorem Finset.singleton_subset_set_iff {α : Type u_1} {s : Set α} {a : α} :
            {a} s a s
            @[simp]
            theorem Finset.singleton_subset_iff {α : Type u_1} {s : Finset α} {a : α} :
            {a} s a s
            @[simp]
            theorem Finset.subset_singleton_iff {α : Type u_1} {s : Finset α} {a : α} :
            s {a} s = s = {a}
            theorem Finset.singleton_subset_singleton {α : Type u_1} {a : α} {b : α} :
            {a} {b} a = b
            theorem Finset.Nonempty.subset_singleton_iff {α : Type u_1} {s : Finset α} {a : α} (h : s.Nonempty) :
            s {a} s = {a}
            theorem Finset.subset_singleton_iff' {α : Type u_1} {s : Finset α} {a : α} :
            s {a} bs, b = a
            @[simp]
            theorem Finset.ssubset_singleton_iff {α : Type u_1} {s : Finset α} {a : α} :
            s {a} s =
            theorem Finset.eq_empty_of_ssubset_singleton {α : Type u_1} {s : Finset α} {x : α} (hs : s {x}) :
            s =
            @[reducible]
            def Finset.Nontrivial {α : Type u_1} (s : Finset α) :

            A finset is nontrivial if it has at least two elements.

            Equations
            Instances For
              @[simp]
              theorem Finset.Nontrivial.ne_singleton {α : Type u_1} {s : Finset α} {a : α} (hs : Finset.Nontrivial s) :
              s {a}
              theorem Finset.Nontrivial.exists_ne {α : Type u_1} {s : Finset α} (hs : Finset.Nontrivial s) (a : α) :
              ∃ b ∈ s, b a
              theorem Finset.eq_singleton_or_nontrivial {α : Type u_1} {s : Finset α} {a : α} (ha : a s) :
              theorem Finset.nontrivial_iff_ne_singleton {α : Type u_1} {s : Finset α} {a : α} (ha : a s) :
              theorem Finset.Nonempty.exists_eq_singleton_or_nontrivial {α : Type u_1} {s : Finset α} :
              s.Nonempty(∃ (a : α), s = {a}) Finset.Nontrivial s
              instance Finset.instNontrivial {α : Type u_1} [Nonempty α] :
              Equations
              • =
              instance Finset.instUniqueFinset {α : Type u_1} [IsEmpty α] :
              Equations
              • Finset.instUniqueFinset = { toInhabited := { default := }, uniq := }
              Equations
              @[simp]
              theorem Finset.default_singleton {α : Type u_1} (i : α) :
              default = i

              cons #

              def Finset.cons {α : Type u_1} (a : α) (s : Finset α) (h : as) :

              cons a s h is the set {a} ∪ s containing a and the elements of s. It is the same as insert a s when it is defined, but unlike insert a s it does not require DecidableEq α, and the union is guaranteed to be disjoint.

              Equations
              Instances For
                @[simp]
                theorem Finset.mem_cons {α : Type u_1} {s : Finset α} {a : α} {b : α} {h : as} :
                b Finset.cons a s h b = a b s
                theorem Finset.mem_cons_of_mem {α : Type u_1} {a : α} {b : α} {s : Finset α} {hb : bs} (ha : a s) :
                a Finset.cons b s hb
                theorem Finset.mem_cons_self {α : Type u_1} (a : α) (s : Finset α) {h : as} :
                @[simp]
                theorem Finset.cons_val {α : Type u_1} {s : Finset α} {a : α} (h : as) :
                (Finset.cons a s h).val = a ::ₘ s.val
                theorem Finset.forall_mem_cons {α : Type u_1} {s : Finset α} {a : α} (h : as) (p : αProp) :
                (xFinset.cons a s h, p x) p a xs, p x
                theorem Finset.forall_of_forall_cons {α : Type u_1} {s : Finset α} {a : α} {p : αProp} {h : as} (H : xFinset.cons a s h✝, p x) (x : α) (h : x s) :
                p x

                Useful in proofs by induction.

                @[simp]
                theorem Finset.mk_cons {α : Type u_1} {a : α} {s : Multiset α} (h : Multiset.Nodup (a ::ₘ s)) :
                { val := a ::ₘ s, nodup := h } = Finset.cons a { val := s, nodup := }
                @[simp]
                theorem Finset.cons_empty {α : Type u_1} (a : α) :
                Finset.cons a = {a}
                @[simp]
                theorem Finset.nonempty_cons {α : Type u_1} {s : Finset α} {a : α} (h : as) :
                (Finset.cons a s h).Nonempty
                @[simp]
                theorem Finset.nonempty_mk {α : Type u_1} {m : Multiset α} {hm : Multiset.Nodup m} :
                { val := m, nodup := hm }.Nonempty m 0
                @[simp]
                theorem Finset.coe_cons {α : Type u_1} {a : α} {s : Finset α} {h : as} :
                (Finset.cons a s h) = insert a s
                theorem Finset.subset_cons {α : Type u_1} {s : Finset α} {a : α} (h : as) :
                theorem Finset.ssubset_cons {α : Type u_1} {s : Finset α} {a : α} (h : as) :
                theorem Finset.cons_subset {α : Type u_1} {s : Finset α} {t : Finset α} {a : α} {h : as} :
                Finset.cons a s h t a t s t
                @[simp]
                theorem Finset.cons_subset_cons {α : Type u_1} {s : Finset α} {t : Finset α} {a : α} {hs : as} {ht : at} :
                Finset.cons a s hs Finset.cons a t ht s t
                theorem Finset.ssubset_iff_exists_cons_subset {α : Type u_1} {s : Finset α} {t : Finset α} :
                s t ∃ (a : α) (h : as), Finset.cons a s h t

                disjoint #

                theorem Finset.disjoint_left {α : Type u_1} {s : Finset α} {t : Finset α} :
                Disjoint s t ∀ ⦃a : α⦄, a sat
                theorem Finset.disjoint_right {α : Type u_1} {s : Finset α} {t : Finset α} :
                Disjoint s t ∀ ⦃a : α⦄, a tas
                theorem Finset.disjoint_iff_ne {α : Type u_1} {s : Finset α} {t : Finset α} :
                Disjoint s t as, bt, a b
                @[simp]
                theorem Finset.disjoint_val {α : Type u_1} {s : Finset α} {t : Finset α} :
                theorem Disjoint.forall_ne_finset {α : Type u_1} {s : Finset α} {t : Finset α} {a : α} {b : α} (h : Disjoint s t) (ha : a s) (hb : b t) :
                a b
                theorem Finset.not_disjoint_iff {α : Type u_1} {s : Finset α} {t : Finset α} :
                ¬Disjoint s t ∃ a ∈ s, a t
                theorem Finset.disjoint_of_subset_left {α : Type u_1} {s : Finset α} {t : Finset α} {u : Finset α} (h : s u) (d : Disjoint u t) :
                theorem Finset.disjoint_of_subset_right {α : Type u_1} {s : Finset α} {t : Finset α} {u : Finset α} (h : t u) (d : Disjoint s u) :
                @[simp]
                theorem Finset.disjoint_empty_left {α : Type u_1} (s : Finset α) :
                @[simp]
                theorem Finset.disjoint_empty_right {α : Type u_1} (s : Finset α) :
                @[simp]
                theorem Finset.disjoint_singleton_left {α : Type u_1} {s : Finset α} {a : α} :
                Disjoint {a} s as
                @[simp]
                theorem Finset.disjoint_singleton_right {α : Type u_1} {s : Finset α} {a : α} :
                Disjoint s {a} as
                theorem Finset.disjoint_singleton {α : Type u_1} {a : α} {b : α} :
                Disjoint {a} {b} a b
                theorem Finset.disjoint_self_iff_empty {α : Type u_1} (s : Finset α) :
                @[simp]
                theorem Finset.disjoint_coe {α : Type u_1} {s : Finset α} {t : Finset α} :
                Disjoint s t Disjoint s t
                @[simp]
                theorem Finset.pairwiseDisjoint_coe {α : Type u_1} {ι : Type u_4} {s : Set ι} {f : ιFinset α} :
                (Set.PairwiseDisjoint s fun (i : ι) => (f i)) Set.PairwiseDisjoint s f

                disjoint union #

                def Finset.disjUnion {α : Type u_1} (s : Finset α) (t : Finset α) (h : Disjoint s t) :

                disjUnion s t h is the set such that a ∈ disjUnion s t h iff a ∈ s or a ∈ t. It is the same as s ∪ t, but it does not require decidable equality on the type. The hypothesis ensures that the sets are disjoint.

                Equations
                Instances For
                  @[simp]
                  theorem Finset.mem_disjUnion {α : Type u_4} {s : Finset α} {t : Finset α} {h : Disjoint s t} {a : α} :
                  a Finset.disjUnion s t h a s a t
                  @[simp]
                  theorem Finset.coe_disjUnion {α : Type u_1} {s : Finset α} {t : Finset α} (h : Disjoint s t) :
                  (Finset.disjUnion s t h) = s t
                  theorem Finset.disjUnion_comm {α : Type u_1} (s : Finset α) (t : Finset α) (h : Disjoint s t) :
                  @[simp]
                  theorem Finset.empty_disjUnion {α : Type u_1} (t : Finset α) (h : optParam (Disjoint t) ) :
                  @[simp]
                  theorem Finset.disjUnion_empty {α : Type u_1} (s : Finset α) (h : optParam (Disjoint s ) ) :
                  theorem Finset.singleton_disjUnion {α : Type u_1} (a : α) (t : Finset α) (h : Disjoint {a} t) :
                  theorem Finset.disjUnion_singleton {α : Type u_1} (s : Finset α) (a : α) (h : Disjoint s {a}) :

                  insert #

                  instance Finset.instInsertFinset {α : Type u_1} [DecidableEq α] :
                  Insert α (Finset α)

                  insert a s is the set {a} ∪ s containing a and the elements of s.

                  Equations
                  • Finset.instInsertFinset = { insert := fun (a : α) (s : Finset α) => { val := Multiset.ndinsert a s.val, nodup := } }
                  theorem Finset.insert_def {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                  insert a s = { val := Multiset.ndinsert a s.val, nodup := }
                  @[simp]
                  theorem Finset.insert_val {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                  (insert a s).val = Multiset.ndinsert a s.val
                  theorem Finset.insert_val' {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                  (insert a s).val = Multiset.dedup (a ::ₘ s.val)
                  theorem Finset.insert_val_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : as) :
                  (insert a s).val = a ::ₘ s.val
                  @[simp]
                  theorem Finset.mem_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} :
                  a insert b s a = b a s
                  theorem Finset.mem_insert_self {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                  a insert a s
                  theorem Finset.mem_insert_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (h : a s) :
                  a insert b s
                  theorem Finset.mem_of_mem_insert_of_ne {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (h : b insert a s) :
                  b ab s
                  theorem Finset.eq_of_not_mem_of_mem_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (ha : b insert a s) (hb : bs) :
                  b = a
                  @[simp]
                  theorem Finset.insert_empty {α : Type u_1} [DecidableEq α] {a : α} :
                  insert a = {a}

                  A version of IsLawfulSingleton.insert_emptyc_eq that works with dsimp.

                  @[simp]
                  theorem Finset.cons_eq_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (h : as) :
                  Finset.cons a s h = insert a s
                  @[simp]
                  theorem Finset.coe_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                  (insert a s) = insert a s
                  theorem Finset.mem_insert_coe {α : Type u_1} [DecidableEq α] {s : Finset α} {x : α} {y : α} :
                  x insert y s x insert y s
                  @[simp]
                  theorem Finset.insert_eq_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a s) :
                  insert a s = s
                  @[simp]
                  theorem Finset.insert_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :
                  insert a s = s a s
                  theorem Finset.insert_ne_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :
                  insert a s s as
                  theorem Finset.pair_eq_singleton {α : Type u_1} [DecidableEq α] (a : α) :
                  {a, a} = {a}
                  theorem Finset.Insert.comm {α : Type u_1} [DecidableEq α] (a : α) (b : α) (s : Finset α) :
                  insert a (insert b s) = insert b (insert a s)
                  theorem Finset.coe_pair {α : Type u_1} [DecidableEq α] {a : α} {b : α} :
                  {a, b} = {a, b}
                  @[simp]
                  theorem Finset.coe_eq_pair {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} :
                  s = {a, b} s = {a, b}
                  theorem Finset.pair_comm {α : Type u_1} [DecidableEq α] (a : α) (b : α) :
                  {a, b} = {b, a}
                  theorem Finset.insert_idem {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                  insert a (insert a s) = insert a s
                  @[simp]
                  theorem Finset.insert_nonempty {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                  (insert a s).Nonempty
                  @[simp]
                  theorem Finset.insert_ne_empty {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                  instance Finset.instNonemptyElemToSetInsertFinsetInstInsertFinset {α : Type u_1} [DecidableEq α] (i : α) (s : Finset α) :
                  Nonempty (insert i s)
                  Equations
                  • =
                  theorem Finset.ne_insert_of_not_mem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) {a : α} (h : as) :
                  s insert a t
                  theorem Finset.insert_subset_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} :
                  insert a s t a t s t
                  theorem Finset.insert_subset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : a t) (hs : s t) :
                  insert a s t
                  @[simp]
                  theorem Finset.subset_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                  s insert a s
                  theorem Finset.insert_subset_insert {α : Type u_1} [DecidableEq α] (a : α) {s : Finset α} {t : Finset α} (h : s t) :
                  insert a s insert a t
                  @[simp]
                  theorem Finset.insert_subset_insert_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : as) :
                  insert a s insert a t s t
                  theorem Finset.insert_inj {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (ha : as) :
                  insert a s = insert b s a = b
                  theorem Finset.insert_inj_on {α : Type u_1} [DecidableEq α] (s : Finset α) :
                  Set.InjOn (fun (a : α) => insert a s) (s)
                  theorem Finset.ssubset_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                  s t ∃ a ∉ s, insert a s t
                  theorem Finset.ssubset_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : as) :
                  s insert a s
                  theorem Finset.cons_induction {α : Type u_4} {p : Finset αProp} (empty : p ) (cons : ∀ ⦃a : α⦄ {s : Finset α} (h : as), p sp (Finset.cons a s h)) (s : Finset α) :
                  p s
                  theorem Finset.cons_induction_on {α : Type u_4} {p : Finset αProp} (s : Finset α) (h₁ : p ) (h₂ : ∀ ⦃a : α⦄ {s : Finset α} (h : as), p sp (Finset.cons a s h)) :
                  p s
                  theorem Finset.induction {α : Type u_4} {p : Finset αProp} [DecidableEq α] (empty : p ) (insert : ∀ ⦃a : α⦄ {s : Finset α}, asp sp (Insert.insert a s)) (s : Finset α) :
                  p s
                  theorem Finset.induction_on {α : Type u_4} {p : Finset αProp} [DecidableEq α] (s : Finset α) (empty : p ) (insert : ∀ ⦃a : α⦄ {s : Finset α}, asp sp (Insert.insert a s)) :
                  p s

                  To prove a proposition about an arbitrary Finset α, it suffices to prove it for the empty Finset, and to show that if it holds for some Finset α, then it holds for the Finset obtained by inserting a new element.

                  theorem Finset.induction_on' {α : Type u_4} {p : Finset αProp} [DecidableEq α] (S : Finset α) (h₁ : p ) (h₂ : ∀ {a : α} {s : Finset α}, a Ss Sasp sp (insert a s)) :
                  p S

                  To prove a proposition about S : Finset α, it suffices to prove it for the empty Finset, and to show that if it holds for some Finset α ⊆ S, then it holds for the Finset obtained by inserting a new element of S.

                  theorem Finset.Nonempty.cons_induction {α : Type u_4} {p : (s : Finset α) → s.NonemptyProp} (h₀ : ∀ (a : α), p {a} ) (h₁ : ∀ ⦃a : α⦄ (s : Finset α) (h : as) (hs : s.Nonempty), p s hsp (Finset.cons a s h) ) {s : Finset α} (hs : s.Nonempty) :
                  p s hs

                  To prove a proposition about a nonempty s : Finset α, it suffices to show it holds for all singletons and that if it holds for nonempty t : Finset α, then it also holds for the Finset obtained by inserting an element in t.

                  theorem Finset.Nonempty.exists_cons_eq {α : Type u_1} [DecidableEq α] {s : Finset α} (hs : s.Nonempty) :
                  ∃ (t : Finset α) (a : α) (ha : at), Finset.cons a t ha = s
                  def Finset.subtypeInsertEquivOption {α : Type u_1} [DecidableEq α] {t : Finset α} {x : α} (h : xt) :
                  { i : α // i insert x t } Option { i : α // i t }

                  Inserting an element to a finite set is equivalent to the option type.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem Finset.disjoint_insert_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} :
                    Disjoint (insert a s) t at Disjoint s t
                    @[simp]
                    theorem Finset.disjoint_insert_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} :
                    Disjoint s (insert a t) as Disjoint s t

                    Lattice structure #

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

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

                    Equations
                    • Finset.instUnionFinset = { union := fun (s t : Finset α) => { val := Multiset.ndunion s.val t.val, nodup := } }
                    instance Finset.instInterFinset {α : Type u_1} [DecidableEq α] :

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

                    Equations
                    • Finset.instInterFinset = { inter := fun (s t : Finset α) => { val := Multiset.ndinter s.val t.val, nodup := } }
                    instance Finset.instLatticeFinset {α : Type u_1} [DecidableEq α] :
                    Equations
                    • Finset.instLatticeFinset = let __src := Finset.partialOrder; Lattice.mk
                    @[simp]
                    theorem Finset.sup_eq_union {α : Type u_1} [DecidableEq α] :
                    Sup.sup = Union.union
                    @[simp]
                    theorem Finset.inf_eq_inter {α : Type u_1} [DecidableEq α] :
                    Inf.inf = Inter.inter
                    theorem Finset.disjoint_iff_inter_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    Disjoint s t s t =
                    instance Finset.decidableDisjoint {α : Type u_1} [DecidableEq α] (U : Finset α) (V : Finset α) :
                    Equations

                    union #

                    theorem Finset.union_val_nd {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                    (s t).val = Multiset.ndunion s.val t.val
                    @[simp]
                    theorem Finset.union_val {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                    (s t).val = s.val t.val
                    @[simp]
                    theorem Finset.mem_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} :
                    a s t a s a t
                    @[simp]
                    theorem Finset.disjUnion_eq_union {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (h : Disjoint s 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 : Finset α} {t : Finset α} {p : αProp} :
                    (as t, p a) (as, p a) at, p a
                    theorem Finset.not_mem_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} :
                    as t as at
                    @[simp]
                    theorem Finset.coe_union {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                    (s₁ s₂) = s₁ s₂
                    theorem Finset.union_subset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (hs : s u) :
                    t us t u
                    theorem Finset.subset_union_left {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                    s₁ s₁ s₂
                    theorem Finset.subset_union_right {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                    s₂ s₁ s₂
                    theorem Finset.union_subset_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} {v : Finset α} (hsu : s u) (htv : t v) :
                    s t u v
                    theorem Finset.union_subset_union_left {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} (h : s₁ s₂) :
                    s₁ t s₂ t
                    theorem Finset.union_subset_union_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} (h : t₁ t₂) :
                    s t₁ s t₂
                    theorem Finset.union_comm {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                    s₁ s₂ = s₂ s₁
                    Equations
                    • =
                    @[simp]
                    theorem Finset.union_assoc {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (s₃ : Finset α) :
                    s₁ s₂ s₃ = s₁ (s₂ s₃)
                    Equations
                    • =
                    @[simp]
                    theorem Finset.union_idempotent {α : Type u_1} [DecidableEq α] (s : Finset α) :
                    s s = s
                    Equations
                    • =
                    theorem Finset.union_subset_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (h : s t u) :
                    s u
                    theorem Finset.union_subset_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (h : s t u) :
                    t u
                    theorem Finset.union_left_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) :
                    s (t u) = t (s u)
                    theorem Finset.union_right_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (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_empty {α : Type u_1} [DecidableEq α] (s : Finset α) :
                    s = s
                    @[simp]
                    theorem Finset.empty_union {α : Type u_1} [DecidableEq α] (s : Finset α) :
                    s = s
                    theorem Finset.Nonempty.inl {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s.Nonempty) :
                    (s t).Nonempty
                    theorem Finset.Nonempty.inr {α : Type u_1} [DecidableEq α] {s : Finset α} {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.insert_union {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) :
                    insert a s t = insert a (s t)
                    @[simp]
                    theorem Finset.union_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) :
                    s insert a t = insert a (s t)
                    theorem Finset.insert_union_distrib {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) :
                    insert a (s t) = insert a s insert a t
                    @[simp]
                    theorem Finset.union_eq_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    s t = s t s
                    @[simp]
                    theorem Finset.left_eq_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    s = s t t s
                    @[simp]
                    theorem Finset.union_eq_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    s t = t s t
                    @[simp]
                    theorem Finset.right_eq_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    s = t s t s
                    theorem Finset.union_congr_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (ht : t s u) (hu : u s t) :
                    s t = s u
                    theorem Finset.union_congr_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {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 : Finset α} {t : Finset α} {u : Finset α} :
                    s t = s u t s u u s t
                    theorem Finset.union_eq_union_iff_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                    s u = t u s t u t s u
                    @[simp]
                    theorem Finset.disjoint_union_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                    @[simp]
                    theorem Finset.disjoint_union_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                    theorem Finset.induction_on_union {α : Type u_1} [DecidableEq α] (P : Finset αFinset αProp) (symm : ∀ {a b : Finset α}, P a bP b a) (empty_right : ∀ {a : Finset α}, P a ) (singletons : ∀ {a b : α}, P {a} {b}) (union_of : ∀ {a b c : Finset α}, P a cP b cP (a b) c) (a : Finset α) (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].
                    theorem Directed.exists_mem_subset_of_finset_subset_biUnion {α : Type u_4} {ι : Type u_5} [hn : Nonempty ι] {f : ιSet α} (h : Directed (fun (x x_1 : Set α) => x x_1) f) {s : Finset α} (hs : s ⋃ (i : ι), f i) :
                    ∃ (i : ι), s f i
                    theorem DirectedOn.exists_mem_subset_of_finset_subset_biUnion {α : Type u_4} {ι : Type u_5} {f : ιSet α} {c : Set ι} (hn : Set.Nonempty c) (hc : DirectedOn (fun (i j : ι) => f i f j) c) {s : Finset α} (hs : s ⋃ i ∈ c, f i) :
                    ∃ i ∈ c, s f i

                    inter #

                    theorem Finset.inter_val_nd {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                    (s₁ s₂).val = Multiset.ndinter s₁.val s₂.val
                    @[simp]
                    theorem Finset.inter_val {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                    (s₁ s₂).val = s₁.val s₂.val
                    @[simp]
                    theorem Finset.mem_inter {α : Type u_1} [DecidableEq α] {a : α} {s₁ : Finset α} {s₂ : Finset α} :
                    a s₁ s₂ a s₁ a s₂
                    theorem Finset.mem_of_mem_inter_left {α : Type u_1} [DecidableEq α] {a : α} {s₁ : Finset α} {s₂ : Finset α} (h : a s₁ s₂) :
                    a s₁
                    theorem Finset.mem_of_mem_inter_right {α : Type u_1} [DecidableEq α] {a : α} {s₁ : Finset α} {s₂ : Finset α} (h : a s₁ s₂) :
                    a s₂
                    theorem Finset.mem_inter_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s₁ : Finset α} {s₂ : Finset α} :
                    a s₁a s₂a s₁ s₂
                    theorem Finset.inter_subset_left {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                    s₁ s₂ s₁
                    theorem Finset.inter_subset_right {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                    s₁ s₂ s₂
                    theorem Finset.subset_inter {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} {u : Finset α} :
                    s₁ s₂s₁ us₁ s₂ u
                    @[simp]
                    theorem Finset.coe_inter {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                    (s₁ s₂) = s₁ s₂
                    @[simp]
                    theorem Finset.union_inter_cancel_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    (s t) s = s
                    @[simp]
                    theorem Finset.union_inter_cancel_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    (s t) t = t
                    theorem Finset.inter_comm {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                    s₁ s₂ = s₂ s₁
                    @[simp]
                    theorem Finset.inter_assoc {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (s₃ : Finset α) :
                    s₁ s₂ s₃ = s₁ (s₂ s₃)
                    theorem Finset.inter_left_comm {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (s₃ : Finset α) :
                    s₁ (s₂ s₃) = s₂ (s₁ s₃)
                    theorem Finset.inter_right_comm {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (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_empty {α : Type u_1} [DecidableEq α] (s : Finset α) :
                    @[simp]
                    theorem Finset.empty_inter {α : Type u_1} [DecidableEq α] (s : Finset α) :
                    @[simp]
                    theorem Finset.inter_union_self {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                    s (t s) = s
                    @[simp]
                    theorem Finset.insert_inter_of_mem {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {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₁ : Finset α} {s₂ : Finset α} {a : α} (h : a s₁) :
                    s₁ insert a s₂ = insert a (s₁ s₂)
                    @[simp]
                    theorem Finset.insert_inter_of_not_mem {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} {a : α} (h : as₂) :
                    insert a s₁ s₂ = s₁ s₂
                    @[simp]
                    theorem Finset.inter_insert_of_not_mem {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} {a : α} (h : as₁) :
                    s₁ insert a s₂ = 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_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (H : as) :
                    {a} s =
                    @[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_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : as) :
                    s {a} =
                    theorem Finset.inter_subset_inter {α : Type u_1} [DecidableEq α] {x : Finset α} {y : Finset α} {s : Finset α} {t : Finset α} (h : x y) (h' : s t) :
                    x s y t
                    theorem Finset.inter_subset_inter_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (h : t u) :
                    s t s u
                    theorem Finset.inter_subset_inter_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (h : s t) :
                    s u t u
                    theorem Finset.inter_subset_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    s t s t
                    Equations
                    @[simp]
                    theorem Finset.union_left_idem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                    s (s t) = s t
                    theorem Finset.union_right_idem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                    s t t = s t
                    @[simp]
                    theorem Finset.inter_left_idem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                    s (s t) = s t
                    theorem Finset.inter_right_idem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                    s t t = s t
                    theorem Finset.inter_union_distrib_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) :
                    s (t u) = s t s u
                    theorem Finset.union_inter_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) :
                    (s t) u = s u t u
                    theorem Finset.union_inter_distrib_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) :
                    s t u = (s t) (s u)
                    theorem Finset.inter_union_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (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 : Finset α) (t : Finset α) (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 : Finset α) (t : Finset α) (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 : Finset α) (t : Finset α) (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 : Finset α) (t : Finset α) (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 : Finset α) (t : Finset α) (u : Finset α) :
                    s (t u) = s t (s u)
                    theorem Finset.union_union_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) :
                    s t u = s u (t u)
                    theorem Finset.inter_inter_distrib_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) :
                    s (t u) = s t (s u)
                    theorem Finset.inter_inter_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) :
                    s t u = s u (t u)
                    theorem Finset.union_union_union_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) (v : Finset α) :
                    s t (u v) = s u (t v)
                    theorem Finset.inter_inter_inter_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) (v : Finset α) :
                    s t (u v) = s u (t v)
                    theorem Finset.union_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    s t = s = t =
                    theorem Finset.union_subset_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                    s t u s u t u
                    theorem Finset.subset_inter_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                    s t u s t s u
                    @[simp]
                    theorem Finset.inter_eq_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    s t = s s t
                    @[simp]
                    theorem Finset.inter_eq_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    t s = s s t
                    theorem Finset.inter_congr_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (ht : s u t) (hu : s t u) :
                    s t = s u
                    theorem Finset.inter_congr_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {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 : Finset α} {t : Finset α} {u : Finset α} :
                    s t = s u s u t s t u
                    theorem Finset.inter_eq_inter_iff_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                    s u = t u t u s s u t
                    theorem Finset.ite_subset_union {α : Type u_1} [DecidableEq α] (s : Finset α) (s' : Finset α) (P : Prop) [Decidable P] :
                    (if P then s else s') s s'
                    theorem Finset.inter_subset_ite {α : Type u_1} [DecidableEq α] (s : Finset α) (s' : Finset α) (P : Prop) [Decidable P] :
                    s s' if P then s else s'
                    theorem Finset.not_disjoint_iff_nonempty_inter {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    ¬Disjoint s t (s t).Nonempty
                    theorem Finset.Nonempty.not_disjoint {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                    (s t).Nonempty¬Disjoint s t

                    Alias of the reverse direction of Finset.not_disjoint_iff_nonempty_inter.

                    theorem Finset.disjoint_or_nonempty_inter {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                    Disjoint s t (s t).Nonempty
                    instance Finset.isDirected_le {α : Type u_1} :
                    IsDirected (Finset α) fun (x x_1 : Finset α) => x x_1
                    Equations
                    • =
                    instance Finset.isDirected_subset {α : Type u_1} :
                    IsDirected (Finset α) fun (x x_1 : Finset α) => x x_1
                    Equations
                    • =

                    erase #

                    def Finset.erase {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :

                    erase s a is the set s - {a}, that is, the elements of s which are not equal to a.

                    Equations
                    Instances For
                      @[simp]
                      theorem Finset.erase_val {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
                      (Finset.erase s a).val = Multiset.erase s.val a
                      @[simp]
                      theorem Finset.mem_erase {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Finset α} :
                      a Finset.erase s b a b a s
                      theorem Finset.not_mem_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                      aFinset.erase s a
                      @[simp]
                      theorem Finset.erase_empty {α : Type u_1} [DecidableEq α] (a : α) :
                      theorem Finset.Nontrivial.erase_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (hs : Finset.Nontrivial s) :
                      (Finset.erase s a).Nonempty
                      @[simp]
                      theorem Finset.erase_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a s) :
                      @[simp]
                      theorem Finset.erase_singleton {α : Type u_1} [DecidableEq α] (a : α) :
                      theorem Finset.ne_of_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} :
                      b Finset.erase s ab a
                      theorem Finset.mem_of_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} :
                      b Finset.erase s ab s
                      theorem Finset.mem_erase_of_ne_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} :
                      a ba sa Finset.erase s b
                      theorem Finset.eq_of_mem_of_not_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (hs : b s) (hsa : bFinset.erase s a) :
                      b = a

                      An element of s that is not an element of erase s a must bea.

                      @[simp]
                      theorem Finset.erase_eq_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : as) :
                      @[simp]
                      theorem Finset.erase_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :
                      Finset.erase s a = s as
                      @[simp]
                      theorem Finset.erase_insert_eq_erase {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
                      theorem Finset.erase_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : as) :
                      theorem Finset.erase_insert_of_ne {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Finset α} (h : a b) :
                      theorem Finset.erase_cons_of_ne {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Finset α} (ha : as) (hb : a b) :
                      @[simp]
                      theorem Finset.insert_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a s) :
                      theorem Finset.erase_eq_iff_eq_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (hs : a s) (ht : at) :
                      Finset.erase s a = t s = insert a t
                      theorem Finset.insert_erase_invOn {α : Type u_1} [DecidableEq α] {a : α} :
                      Set.InvOn (insert a) (fun (s : Finset α) => Finset.erase s a) {s : Finset α | a s} {s : Finset α | as}
                      theorem Finset.erase_subset_erase {α : Type u_1} [DecidableEq α] (a : α) {s : Finset α} {t : Finset α} (h : s t) :
                      theorem Finset.erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                      theorem Finset.subset_erase {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} {t : Finset α} :
                      s Finset.erase t a s t as
                      @[simp]
                      theorem Finset.coe_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                      (Finset.erase s a) = s \ {a}
                      theorem Finset.erase_ssubset {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a s) :
                      theorem Finset.ssubset_iff_exists_subset_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      s t ∃ a ∈ t, s Finset.erase t a
                      theorem Finset.erase_ssubset_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
                      theorem Finset.erase_ne_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :
                      theorem Finset.erase_cons {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : as) :
                      theorem Finset.erase_idem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} :
                      theorem Finset.erase_right_comm {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Finset α} :
                      theorem Finset.subset_insert_iff {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} {t : Finset α} :
                      theorem Finset.erase_insert_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                      theorem Finset.insert_erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                      theorem Finset.subset_insert_iff_of_not_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (h : as) :
                      s insert a t s t
                      theorem Finset.erase_subset_iff_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (h : a t) :
                      theorem Finset.erase_inj {α : Type u_1} [DecidableEq α] {x : α} {y : α} (s : Finset α) (hx : x s) :
                      theorem Finset.erase_injOn {α : Type u_1} [DecidableEq α] (s : Finset α) :
                      theorem Finset.erase_injOn' {α : Type u_1} [DecidableEq α] (a : α) :
                      Set.InjOn (fun (s : Finset α) => Finset.erase s a) {s : Finset α | a s}
                      theorem Finset.Nontrivial.exists_cons_eq {α : Type u_1} {s : Finset α} (hs : Finset.Nontrivial s) :
                      ∃ (t : Finset α) (a : α) (ha : at) (b : α) (hb : bt) (hab : ¬a = b), Finset.cons a (Finset.cons b t hb) = s

                      sdiff #

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

                      s \ t is the set consisting of the elements of s that are not in t.

                      Equations
                      • Finset.instSDiffFinset = { sdiff := fun (s₁ s₂ : Finset α) => { val := s₁.val - s₂.val, nodup := } }
                      @[simp]
                      theorem Finset.sdiff_val {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                      (s₁ \ s₂).val = s₁.val - s₂.val
                      @[simp]
                      theorem Finset.mem_sdiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} :
                      a s \ t a s at
                      @[simp]
                      theorem Finset.inter_sdiff_self {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                      s₁ (s₂ \ s₁) =
                      Equations
                      theorem Finset.not_mem_sdiff_of_mem_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (h : a t) :
                      as \ t
                      theorem Finset.not_mem_sdiff_of_not_mem_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (h : as) :
                      as \ t
                      theorem Finset.union_sdiff_of_subset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s t) :
                      s t \ s = t
                      theorem Finset.sdiff_union_of_subset {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} (h : s₁ s₂) :
                      s₂ \ s₁ s₁ = s₂
                      theorem Finset.inter_sdiff {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) :
                      s (t \ u) = (s t) \ u
                      @[simp]
                      theorem Finset.sdiff_inter_self {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                      s₂ \ s₁ s₁ =
                      theorem Finset.sdiff_self {α : Type u_1} [DecidableEq α] (s₁ : Finset α) :
                      s₁ \ s₁ =
                      theorem Finset.sdiff_inter_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) :
                      s \ (t u) = s \ t s \ u
                      @[simp]
                      theorem Finset.sdiff_inter_self_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      s \ (s t) = s \ t
                      @[simp]
                      theorem Finset.sdiff_inter_self_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      s \ (t s) = s \ t
                      @[simp]
                      theorem Finset.sdiff_empty {α : Type u_1} [DecidableEq α] {s : Finset α} :
                      s \ = s
                      theorem Finset.sdiff_subset_sdiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} {v : Finset α} (hst : s t) (hvu : v u) :
                      s \ u t \ v
                      @[simp]
                      theorem Finset.coe_sdiff {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                      (s₁ \ s₂) = s₁ \ s₂
                      @[simp]
                      theorem Finset.union_sdiff_self_eq_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      s t \ s = s t
                      @[simp]
                      theorem Finset.sdiff_union_self_eq_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      s \ t t = s t
                      theorem Finset.union_sdiff_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      (s t) \ s = t \ s
                      theorem Finset.union_sdiff_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      (s t) \ t = s \ t
                      theorem Finset.union_sdiff_cancel_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) :
                      (s t) \ s = t
                      theorem Finset.union_sdiff_cancel_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) :
                      (s t) \ t = s
                      theorem Finset.union_sdiff_symm {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      s t \ s = t s \ t
                      theorem Finset.sdiff_union_inter {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      s \ t s t = s
                      theorem Finset.sdiff_idem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      (s \ t) \ t = s \ t
                      theorem Finset.subset_sdiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                      s t \ u s t Disjoint s u
                      @[simp]
                      theorem Finset.sdiff_eq_empty_iff_subset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      s \ t = s t
                      theorem Finset.sdiff_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      (s \ t).Nonempty ¬s t
                      @[simp]
                      theorem Finset.empty_sdiff {α : Type u_1} [DecidableEq α] (s : Finset α) :
                      theorem Finset.insert_sdiff_of_not_mem {α : Type u_1} [DecidableEq α] (s : Finset α) {t : Finset α} {x : α} (h : xt) :
                      insert x s \ t = insert x (s \ t)
                      theorem Finset.insert_sdiff_of_mem {α : Type u_1} [DecidableEq α] {t : Finset α} (s : Finset α) {x : α} (h : x t) :
                      insert x s \ t = s \ t
                      @[simp]
                      theorem Finset.insert_sdiff_cancel {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : as) :
                      insert a s \ s = {a}
                      @[simp]
                      theorem Finset.insert_sdiff_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (x : α) :
                      insert x s \ insert x t = s \ insert x t
                      theorem Finset.insert_sdiff_insert' {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (hab : a b) (ha : as) :
                      insert a s \ insert b s = {a}
                      theorem Finset.erase_sdiff_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (hab : a b) (hb : b s) :
                      theorem Finset.cons_sdiff_cons {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (hab : a b) (ha : as) (hb : bs) :
                      Finset.cons a s ha \ Finset.cons b s hb = {a}
                      theorem Finset.sdiff_insert_of_not_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {x : α} (h : xs) (t : Finset α) :
                      s \ insert x t = s \ t
                      @[simp]
                      theorem Finset.sdiff_subset {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      s \ t s
                      theorem Finset.sdiff_ssubset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : t s) (ht : t.Nonempty) :
                      s \ t s
                      theorem Finset.union_sdiff_distrib {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (t : Finset α) :
                      (s₁ s₂) \ t = s₁ \ t s₂ \ t
                      theorem Finset.sdiff_union_distrib {α : Type u_1} [DecidableEq α] (s : Finset α) (t₁ : Finset α) (t₂ : Finset α) :
                      s \ (t₁ t₂) = s \ t₁ (s \ t₂)
                      theorem Finset.union_sdiff_self {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      (s t) \ t = s \ t
                      theorem Finset.sdiff_singleton_eq_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
                      s \ {a} = Finset.erase s a
                      theorem Finset.erase_eq {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
                      Finset.erase s a = s \ {a}
                      theorem Finset.disjoint_erase_comm {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} :
                      theorem Finset.disjoint_insert_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : at) :
                      theorem Finset.disjoint_erase_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : as) :
                      theorem Finset.disjoint_of_erase_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : at) (hst : Disjoint (Finset.erase s a) t) :
                      theorem Finset.disjoint_of_erase_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : as) (hst : Disjoint s (Finset.erase t a)) :
                      theorem Finset.inter_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) :
                      @[simp]
                      theorem Finset.erase_inter {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) :
                      theorem Finset.erase_sdiff_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) :
                      Finset.erase s a \ t = Finset.erase (s \ t) a
                      theorem Finset.insert_union_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) :
                      insert a s t = s insert a t
                      theorem Finset.erase_inter_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) :
                      theorem Finset.erase_union_distrib {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) :
                      theorem Finset.insert_inter_distrib {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) :
                      insert a (s t) = insert a s insert a t
                      theorem Finset.erase_sdiff_distrib {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) :
                      theorem Finset.erase_union_of_mem {α : Type u_1} [DecidableEq α] {t : Finset α} {a : α} (ha : a t) (s : Finset α) :
                      Finset.erase s a t = s t
                      theorem Finset.union_erase_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a s) (t : Finset α) :
                      s Finset.erase t a = s t
                      @[simp]
                      theorem Finset.sdiff_singleton_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : as) :
                      s \ {a} = s
                      theorem Finset.Nontrivial.sdiff_singleton_nonempty {α : Type u_1} [DecidableEq α] {c : α} {s : Finset α} (hS : Finset.Nontrivial s) :
                      (s \ {c}).Nonempty
                      theorem Finset.sdiff_sdiff_left' {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) :
                      (s \ t) \ u = s \ t (s \ u)
                      theorem Finset.sdiff_union_sdiff_cancel {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (hts : t s) (hut : u t) :
                      s \ t t \ u = s \ u
                      theorem Finset.sdiff_union_erase_cancel {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (hts : t s) (ha : a t) :
                      theorem Finset.sdiff_sdiff_eq_sdiff_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (h : u s) :
                      s \ (t \ u) = s \ t u
                      theorem Finset.sdiff_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (x : α) :
                      s \ insert x t = Finset.erase (s \ t) x
                      theorem Finset.sdiff_insert_insert_of_mem_of_not_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {x : α} (hxs : x s) (hxt : xt) :
                      insert x (s \ insert x t) = s \ t
                      theorem Finset.sdiff_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (h : a s) :
                      s \ Finset.erase t a = insert a (s \ t)
                      theorem Finset.sdiff_erase_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a s) :
                      s \ Finset.erase s a = {a}
                      theorem Finset.sdiff_sdiff_self_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      s \ (s \ t) = s t
                      theorem Finset.sdiff_sdiff_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : t s) :
                      s \ (s \ t) = t
                      theorem Finset.sdiff_eq_sdiff_iff_inter_eq_inter {α : Type u_1} [DecidableEq α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      s \ t₁ = s \ t₂ s t₁ = s t₂
                      theorem Finset.union_eq_sdiff_union_sdiff_union_inter {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      s t = s \ t t \ s s t
                      theorem Finset.erase_eq_empty_iff {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
                      Finset.erase s a = s = s = {a}
                      theorem Finset.sdiff_disjoint {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      Disjoint (t \ s) s
                      theorem Finset.disjoint_sdiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      Disjoint s (t \ s)
                      theorem Finset.disjoint_sdiff_inter {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
                      Disjoint (s \ t) (s t)
                      theorem Finset.sdiff_eq_self_iff_disjoint {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      s \ t = s Disjoint s t
                      theorem Finset.sdiff_eq_self_of_disjoint {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) :
                      s \ t = s

                      Symmetric difference #

                      theorem Finset.mem_symmDiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} :
                      a symmDiff s t a s at a t as
                      @[simp]
                      theorem Finset.coe_symmDiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      (symmDiff s t) = symmDiff s t
                      @[simp]
                      theorem Finset.symmDiff_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      symmDiff s t = s = t
                      @[simp]
                      theorem Finset.symmDiff_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                      (symmDiff s t).Nonempty s t

                      attach #

                      def Finset.attach {α : Type u_1} (s : Finset α) :
                      Finset { x : α // x s }

                      attach s takes the elements of s and forms a new set of elements of the subtype {x // x ∈ s}.

                      Equations
                      Instances For
                        theorem Finset.sizeOf_lt_sizeOf_of_mem {α : Type u_1} [SizeOf α] {x : α} {s : Finset α} (hx : x s) :
                        @[simp]
                        theorem Finset.attach_val {α : Type u_1} (s : Finset α) :
                        @[simp]
                        theorem Finset.mem_attach {α : Type u_1} (s : Finset α) (x : { x : α // x s }) :
                        @[simp]
                        @[simp]
                        theorem Finset.attach_nonempty_iff {α : Type u_1} {s : Finset α} :
                        (Finset.attach s).Nonempty s.Nonempty
                        theorem Finset.Nonempty.attach {α : Type u_1} {s : Finset α} :
                        s.Nonempty(Finset.attach s).Nonempty

                        Alias of the reverse direction of Finset.attach_nonempty_iff.

                        @[simp]
                        theorem Finset.attach_eq_empty_iff {α : Type u_1} {s : Finset α} :

                        piecewise #

                        def Finset.piecewise {α : Type u_4} {δ : αSort u_5} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] (i : α) :
                        δ i

                        s.piecewise f g is the function equal to f on the finset s, and to g on its complement.

                        Equations
                        Instances For
                          theorem Finset.piecewise_insert_self {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [DecidableEq α] {j : α} [(i : α) → Decidable (i insert j s)] :
                          Finset.piecewise (insert j s) f g j = f j
                          @[simp]
                          theorem Finset.piecewise_empty {α : Type u_1} {δ : αSort u_4} (f : (i : α) → δ i) (g : (i : α) → δ i) [(i : α) → Decidable (i )] :
                          theorem Finset.piecewise_coe {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] [(j : α) → Decidable (j s)] :
                          @[simp]
                          theorem Finset.piecewise_eq_of_mem {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] {i : α} (hi : i s) :
                          Finset.piecewise s f g i = f i
                          @[simp]
                          theorem Finset.piecewise_eq_of_not_mem {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] {i : α} (hi : is) :
                          Finset.piecewise s f g i = g i
                          theorem Finset.piecewise_congr {α : Type u_1} {δ : αSort u_4} (s : Finset α) [(j : α) → Decidable (j s)] {f : (i : α) → δ i} {f' : (i : α) → δ i} {g : (i : α) → δ i} {g' : (i : α) → δ i} (hf : is, f i = f' i) (hg : is, g i = g' i) :
                          @[simp]
                          theorem Finset.piecewise_insert_of_ne {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] [DecidableEq α] {i : α} {j : α} [(i : α) → Decidable (i insert j s)] (h : i j) :
                          theorem Finset.piecewise_insert {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] [DecidableEq α] (j : α) [(i : α) → Decidable (i insert j s)] :
                          theorem Finset.piecewise_cases {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] {i : α} (p : δ iProp) (hf : p (f i)) (hg : p (g i)) :
                          p (Finset.piecewise s f g i)
                          theorem Finset.piecewise_mem_set_pi {α : Type u_1} (s : Finset α) [(j : α) → Decidable (j s)] {δ : αType u_5} {t : Set α} {t' : (i : α) → Set (δ i)} {f : (i : α) → δ i} {g : (i : α) → δ i} (hf : f Set.pi t t') (hg : g Set.pi t t') :
                          theorem Finset.piecewise_singleton {α : Type u_1} {δ : αSort u_4} (f : (i : α) → δ i) (g : (i : α) → δ i) [DecidableEq α] (i : α) :
                          theorem Finset.piecewise_piecewise_of_subset_left {α : Type u_1} {δ : αSort u_4} {s : Finset α} {t : Finset α} [(i : α) → Decidable (i s)] [(i : α) → Decidable (i t)] (h : s t) (f₁ : (a : α) → δ a) (f₂ : (a : α) → δ a) (g : (a : α) → δ a) :
                          @[simp]
                          theorem Finset.piecewise_idem_left {α : Type u_1} {δ : αSort u_4} (s : Finset α) [(j : α) → Decidable (j s)] (f₁ : (a : α) → δ a) (f₂ : (a : α) → δ a) (g : (a : α) → δ a) :
                          theorem Finset.piecewise_piecewise_of_subset_right {α : Type u_1} {δ : αSort u_4} {s : Finset α} {t : Finset α} [(i : α) → Decidable (i s)] [(i : α) → Decidable (i t)] (h : t s) (f : (a : α) → δ a) (g₁ : (a : α) → δ a) (g₂ : (a : α) → δ a) :
                          @[simp]
                          theorem Finset.piecewise_idem_right {α : Type u_1} {δ : αSort u_4} (s : Finset α) [(j : α) → Decidable (j s)] (f : (a : α) → δ a) (g₁ : (a : α) → δ a) (g₂ : (a : α) → δ a) :
                          theorem Finset.update_eq_piecewise {α : Type u_1} {β : Type u_5} [DecidableEq α] (f : αβ) (i : α) (v : β) :
                          Function.update f i v = Finset.piecewise {i} (fun (x : α) => v) f
                          theorem Finset.update_piecewise {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] [DecidableEq α] (i : α) (v : δ i) :
                          theorem Finset.update_piecewise_of_mem {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] [DecidableEq α] {i : α} (hi : i s) (v : δ i) :
                          theorem Finset.update_piecewise_of_not_mem {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) (g : (i : α) → δ i) [(j : α) → Decidable (j s)] [DecidableEq α] {i : α} (hi : is) (v : δ i) :
                          theorem Finset.piecewise_le_of_le_of_le {α : Type u_1} (s : Finset α) [(j : α) → Decidable (j s)] {δ : αType u_5} [(i : α) → Preorder (δ i)] {f : (i : α) → δ i} {g : (i : α) → δ i} {h : (i : α) → δ i} (Hf : f h) (Hg : g h) :
                          theorem Finset.le_piecewise_of_le_of_le {α : Type u_1} (s : Finset α) [(j : α) → Decidable (j s)] {δ : αType u_5} [(i : α) → Preorder (δ i)] {f : (i : α) → δ i} {g : (i : α) → δ i} {h : (i : α) → δ i} (Hf : h f) (Hg : h g) :
                          theorem Finset.piecewise_le_piecewise' {α : Type u_1} (s : Finset α) [(j : α) → Decidable (j s)] {δ : αType u_5} [(i : α) → Preorder (δ i)] {f : (i : α) → δ i} {g : (i : α) → δ i} {f' : (i : α) → δ i} {g' : (i : α) → δ i} (Hf : xs, f x f' x) (Hg : xs, g x g' x) :
                          theorem Finset.piecewise_le_piecewise {α : Type u_1} (s : Finset α) [(j : α) → Decidable (j s)] {δ : αType u_5} [(i : α) → Preorder (δ i)] {f : (i : α) → δ i} {g : (i : α) → δ i} {f' : (i : α) → δ i} {g' : (i : α) → δ i} (Hf : f f') (Hg : g g') :
                          theorem Finset.piecewise_mem_Icc_of_mem_of_mem {α : Type u_1} (s : Finset α) [(j : α) → Decidable (j s)] {δ : αType u_5} [(i : α) → Preorder (δ i)] {f : (i : α) → δ i} {f₁ : (i : α) → δ i} {g : (i : α) → δ i} {g₁ : (i : α) → δ i} (hf : f Set.Icc f₁ g₁) (hg : g Set.Icc f₁ g₁) :
                          Finset.piecewise s f g Set.Icc f₁ g₁
                          theorem Finset.piecewise_mem_Icc {α : Type u_1} (s : Finset α) [(j : α) → Decidable (j s)] {δ : αType u_5} [(i : α) → Preorder (δ i)] {f : (i : α) → δ i} {g : (i : α) → δ i} (h : f g) :
                          theorem Finset.piecewise_mem_Icc' {α : Type u_1} (s : Finset α) [(j : α) → Decidable (j s)] {δ : αType u_5} [(i : α) → Preorder (δ i)] {f : (i : α) → δ i} {g : (i : α) → δ i} (h : g f) :
                          theorem Finset.piecewise_same {α : Type u_1} {δ : αSort u_4} (s : Finset α) (f : (i : α) → δ i) [(j : α) → Decidable (j s)] :
                          instance Finset.decidableDforallFinset {α : Type u_1} {s : Finset α} {p : (a : α) → a sProp} [_hp : (a : α) → (h : a s) → Decidable (p a h)] :
                          Decidable (∀ (a : α) (h : a s), p a h)
                          Equations
                          • Finset.decidableDforallFinset = Multiset.decidableDforallMultiset
                          instance Finset.instDecidableRelSubset {α : Type u_1} [DecidableEq α] :
                          DecidableRel fun (x x_1 : Finset α) => x x_1
                          Equations
                          instance Finset.instDecidableRelSSubset {α : Type u_1} [DecidableEq α] :
                          DecidableRel fun (x x_1 : Finset α) => x x_1
                          Equations
                          instance Finset.instDecidableLE {α : Type u_1} [DecidableEq α] :
                          DecidableRel fun (x x_1 : Finset α) => x x_1
                          Equations
                          • Finset.instDecidableLE = Finset.instDecidableRelSubset
                          instance Finset.instDecidableLT {α : Type u_1} [DecidableEq α] :
                          DecidableRel fun (x x_1 : Finset α) => x < x_1
                          Equations
                          • Finset.instDecidableLT = Finset.instDecidableRelSSubset
                          instance Finset.decidableDExistsFinset {α : Type u_1} {s : Finset α} {p : (a : α) → a sProp} [_hp : (a : α) → (h : a s) → Decidable (p a h)] :
                          Decidable (∃ (a : α) (h : a s), p a h)
                          Equations
                          • Finset.decidableDExistsFinset = Multiset.decidableDexistsMultiset
                          instance Finset.decidableExistsAndFinset {α : Type u_1} {s : Finset α} {p : αProp} [_hp : (a : α) → Decidable (p a)] :
                          Decidable (∃ a ∈ s, p a)
                          Equations
                          instance Finset.decidableExistsAndFinsetCoe {α : Type u_1} {s : Finset α} {p : αProp} [DecidablePred p] :
                          Decidable (∃ a ∈ s, p a)
                          Equations
                          • Finset.decidableExistsAndFinsetCoe = Finset.decidableExistsAndFinset
                          instance Finset.decidableEqPiFinset {α : Type u_1} {s : Finset α} {β : αType u_4} [_h : (a : α) → DecidableEq (β a)] :
                          DecidableEq ((a : α) → a sβ a)

                          decidable equality for functions whose domain is bounded by finsets

                          Equations
                          • Finset.decidableEqPiFinset = Multiset.decidableEqPiMultiset

                          filter #

                          def Finset.filter {α : Type u_1} (p : αProp) [DecidablePred p] (s : Finset α) :

                          Finset.filter p s is the set of elements of s that satisfy p.

                          For example, one can use s.filter (· ∈ t) to get the intersection of s with t : Set α as a Finset α (when a DecidablePred (· ∈ t) instance is available).

                          Equations
                          Instances For
                            @[simp]
                            theorem Finset.filter_val {α : Type u_1} (p : αProp) [DecidablePred p] (s : Finset α) :
                            (Finset.filter p s).val = Multiset.filter p s.val
                            @[simp]
                            theorem Finset.filter_subset {α : Type u_1} (p : αProp) [DecidablePred p] (s : Finset α) :
                            @[simp]
                            theorem Finset.mem_filter {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} {a : α} :
                            a Finset.filter p s a s p a
                            theorem Finset.mem_of_mem_filter {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} (x : α) (h : x Finset.filter p s) :
                            x s
                            theorem Finset.filter_ssubset {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} :
                            Finset.filter p s s ∃ x ∈ s, ¬p x
                            theorem Finset.filter_filter {α : Type u_1} (p : αProp) (q : αProp) [DecidablePred p] [DecidablePred q] (s : Finset α) :
                            Finset.filter q (Finset.filter p s) = Finset.filter (fun (a : α) => p a q a) s
                            theorem Finset.filter_comm {α : Type u_1} (p : αProp) (q : αProp) [DecidablePred p] [DecidablePred q] (s : Finset α) :
                            @[simp]
                            theorem Finset.filter_congr_decidable {α : Type u_1} (s : Finset α) (p : αProp) (h : DecidablePred p) [DecidablePred p] :
                            theorem Finset.filter_True {α : Type u_1} {h : DecidablePred fun (x : α) => True} (s : Finset α) :
                            Finset.filter (fun (x : α) => True) s = s
                            theorem Finset.filter_False {α : Type u_1} {h : DecidablePred fun (x : α) => False} (s : Finset α) :
                            Finset.filter (fun (x : α) => False) s =
                            theorem Finset.filter_eq_self {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} :
                            Finset.filter p s = s xs, p x
                            theorem Finset.filter_eq_empty_iff {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} :
                            Finset.filter p s = ∀ ⦃x : α⦄, x s¬p x
                            theorem Finset.filter_nonempty_iff {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} :
                            (Finset.filter p s).Nonempty ∃ a ∈ s, p a
                            @[simp]
                            theorem Finset.filter_true_of_mem {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} (h : xs, p x) :

                            If all elements of a Finset satisfy the predicate p, s.filter p is s.

                            @[simp]
                            theorem Finset.filter_false_of_mem {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} (h : xs, ¬p x) :

                            If all elements of a Finset fail to satisfy the predicate p, s.filter p is .

                            @[simp]
                            theorem Finset.filter_const {α : Type u_1} (p : Prop) [Decidable p] (s : Finset α) :
                            Finset.filter (fun (_a : α) => p) s = if p then s else
                            theorem Finset.filter_congr {α : Type u_1} {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] {s : Finset α} (H : xs, p x q x) :
                            theorem Finset.filter_empty {α : Type u_1} (p : αProp) [DecidablePred p] :
                            theorem Finset.filter_subset_filter {α : Type u_1} (p : αProp) [DecidablePred p] {s : Finset α} {t : Finset α} (h : s t) :
                            theorem Finset.monotone_filter_right {α : Type u_1} (s : Finset α) ⦃p : αProp ⦃q : αProp [DecidablePred p] [DecidablePred q] (h : p q) :
                            @[simp]
                            theorem Finset.coe_filter {α : Type u_1} (p : αProp) [DecidablePred p] (s : Finset α) :
                            (Finset.filter p s) = {x : α | x s p x}
                            theorem Finset.subset_coe_filter_of_subset_forall {α : Type u_1} (p : αProp) [DecidablePred p] (s : Finset α) {t : Set α} (h₁ : t s) (h₂ : xt, p x) :
                            t (Finset.filter p s)
                            theorem Finset.filter_singleton {α : Type u_1} (p : αProp) [DecidablePred p] (a : α) :
                            Finset.filter p {a} = if p a then {a} else
                            theorem Finset.filter_cons_of_pos {α : Type u_1} (p : αProp) [DecidablePred p] (a : α) (s : Finset α) (ha : as) (hp : p a) :
                            theorem Finset.filter_cons_of_neg {α : Type u_1} (p : αProp) [DecidablePred p] (a : α) (s : Finset α) (ha : as) (hp : ¬p a) :
                            theorem Finset.disjoint_filter {α : Type u_1} {s : Finset α} {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] :
                            Disjoint (Finset.filter p s) (Finset.filter q s) xs, p x¬q x
                            theorem Finset.disjoint_filter_filter {α : Type u_1} {s : Finset α} {t : Finset α} {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] :
                            theorem Finset.disjoint_filter_filter' {α : Type u_1} (s : Finset α) (t : Finset α) {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] (h : Disjoint p q) :
                            theorem Finset.disjoint_filter_filter_neg {α : Type u_1} (s : Finset α) (t : Finset α) (p : αProp) [DecidablePred p] [(x : α) → Decidable ¬p x] :
                            Disjoint (Finset.filter p s) (Finset.filter (fun (a : α) => ¬p a) t)
                            theorem Finset.filter_disj_union {α : Type u_1} (p : αProp) [DecidablePred p] (s : Finset α) (t : Finset α) (h : Disjoint s t) :
                            theorem Set.pairwiseDisjoint_filter {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : αβ) (s : Set β) (t : Finset α) :
                            Set.PairwiseDisjoint s fun (x : β) => Finset.filter (fun (x_1 : α) => f x_1 = x) t
                            theorem Finset.filter_cons {α : Type u_1} (p : αProp) [DecidablePred p] {a : α} (s : Finset α) (ha : as) :
                            Finset.filter p (Finset.cons a s ha) = Finset.disjUnion (if p a then {a} else ) (Finset.filter p s)
                            theorem Finset.filter_union {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                            Finset.filter p (s₁ s₂) = Finset.filter p s₁ Finset.filter p s₂
                            theorem Finset.filter_union_right {α : Type u_1} (p : αProp) (q : αProp) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) :
                            Finset.filter p s Finset.filter q s = Finset.filter (fun (x : α) => p x q x) s
                            theorem Finset.filter_mem_eq_inter {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} [(i : α) → Decidable (i t)] :
                            Finset.filter (fun (i : α) => i t) s = s t
                            theorem Finset.filter_inter_distrib {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s : Finset α) (t : Finset α) :
                            theorem Finset.filter_inter {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s : Finset α) (t : Finset α) :
                            theorem Finset.inter_filter {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s : Finset α) (t : Finset α) :
                            theorem Finset.filter_insert {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (a : α) (s : Finset α) :
                            Finset.filter p (insert a s) = if p a then insert a (Finset.filter p s) else Finset.filter p s
                            theorem Finset.filter_erase {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (a : α) (s : Finset α) :
                            theorem Finset.filter_or {α : Type u_1} (p : αProp) (q : αProp) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) :
                            Finset.filter (fun (a : α) => p a q a) s = Finset.filter p s Finset.filter q s
                            theorem Finset.filter_and {α : Type u_1} (p : αProp) (q : αProp) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) :
                            Finset.filter (fun (a : α) => p a q a) s = Finset.filter p s Finset.filter q s
                            theorem Finset.filter_not {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s : Finset α) :
                            Finset.filter (fun (a : α) => ¬p a) s = s \ Finset.filter p s
                            theorem Finset.sdiff_eq_filter {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                            s₁ \ s₂ = Finset.filter (fun (x : α) => xs₂) s₁
                            theorem Finset.sdiff_eq_self {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) :
                            s₁ \ s₂ = s₁ s₁ s₂
                            theorem Finset.subset_union_elim {α : Type u_1} [DecidableEq α] {s : Finset α} {t₁ : Set α} {t₂ : Set α} (h : s t₁ t₂) :
                            ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ s₂ = s s₁ t₁ s₂ t₂ \ t₁
                            theorem Finset.filter_eq {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :
                            Finset.filter (Eq b) s = if b s then {b} else

                            After filtering out everything that does not equal a given value, at most that value remains.

                            This is equivalent to filter_eq' with the equality the other way.

                            theorem Finset.filter_eq' {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :
                            Finset.filter (fun (a : β) => a = b) s = if b s then {b} else

                            After filtering out everything that does not equal a given value, at most that value remains.

                            This is equivalent to filter_eq with the equality the other way.

                            theorem Finset.filter_ne {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :
                            Finset.filter (fun (a : β) => b a) s = Finset.erase s b
                            theorem Finset.filter_ne' {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :
                            Finset.filter (fun (a : β) => a b) s = Finset.erase s b
                            theorem Finset.filter_inter_filter_neg_eq {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s : Finset α) (t : Finset α) :
                            Finset.filter p s Finset.filter (fun (a : α) => ¬p a) t =
                            theorem Finset.filter_union_filter_of_codisjoint {α : Type u_1} (p : αProp) (q : αProp) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) (h : Codisjoint p q) :
                            theorem Finset.filter_union_filter_neg_eq {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] [(x : α) → Decidable ¬p x] (s : Finset α) :
                            Finset.filter p s Finset.filter (fun (a : α) => ¬p a) s = s

                            range #

                            range n is the set of natural numbers less than n.

                            Equations
                            Instances For
                              @[simp]
                              @[simp]
                              theorem Finset.mem_range {n : } {m : } :
                              @[simp]
                              theorem Finset.coe_range (n : ) :
                              @[simp]
                              @[simp]

                              Alias of the reverse direction of Finset.range_subset.

                              theorem Finset.mem_range_le {n : } {x : } (hx : x Finset.range n) :
                              x n
                              theorem Finset.mem_range_sub_ne_zero {n : } {x : } (hx : x Finset.range n) :
                              n - x 0
                              @[simp]
                              theorem Finset.nonempty_range_iff {n : } :
                              (Finset.range n).Nonempty n 0
                              theorem Finset.nonempty_range_succ {n : } :
                              (Finset.range (n + 1)).Nonempty
                              @[simp]
                              theorem Finset.range_filter_eq {n : } {m : } :
                              Finset.filter (fun (x : ) => x = m) (Finset.range n) = if m < n then {m} else
                              theorem Finset.exists_mem_empty_iff {α : Type u_1} (p : αProp) :
                              (∃ x ∈ , p x) False
                              theorem Finset.exists_mem_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (p : αProp) :
                              (∃ x ∈ insert a s, p x) p a ∃ x ∈ s, p x
                              theorem Finset.forall_mem_empty_iff {α : Type u_1} (p : αProp) :
                              (x, p x) True
                              theorem Finset.forall_mem_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (p : αProp) :
                              (xinsert a s, p x) p a xs, p x
                              theorem Finset.forall_of_forall_insert {α : Type u_1} [DecidableEq α] {p : αProp} {a : α} {s : Finset α} (H : xinsert a s, p x) (x : α) (h : x s) :
                              p x

                              Useful in proofs by induction.

                              def notMemRangeEquiv (k : ) :
                              { n : // nMultiset.range k }

                              Equivalence between the set of natural numbers which are ≥ k and , given by n → n - k.

                              Equations
                              Instances For
                                @[simp]
                                theorem coe_notMemRangeEquiv (k : ) :
                                (notMemRangeEquiv k) = fun (i : { n : // nMultiset.range k }) => i - k
                                @[simp]
                                theorem coe_notMemRangeEquiv_symm (k : ) :
                                (notMemRangeEquiv k).symm = fun (j : ) => { val := j + k, property := }

                                dedup on list and multiset #

                                def Multiset.toFinset {α : Type u_1} [DecidableEq α] (s : Multiset α) :

                                toFinset s removes duplicates from the multiset s to produce a finset.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Multiset.toFinset_eq {α : Type u_1} [DecidableEq α] {s : Multiset α} (n : Multiset.Nodup s) :
                                  { val := s, nodup := n } = Multiset.toFinset s
                                  theorem Multiset.Nodup.toFinset_inj {α : Type u_1} [DecidableEq α] {l : Multiset α} {l' : Multiset α} (hl : Multiset.Nodup l) (hl' : Multiset.Nodup l') (h : Multiset.toFinset l = Multiset.toFinset l') :
                                  l = l'
                                  @[simp]
                                  theorem Multiset.mem_toFinset {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                  @[simp]
                                  theorem Multiset.toFinset_cons {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
                                  @[simp]
                                  theorem Multiset.toFinset_singleton {α : Type u_1} [DecidableEq α] (a : α) :
                                  @[simp]
                                  theorem Multiset.toFinset_nsmul {α : Type u_1} [DecidableEq α] (s : Multiset α) (n : ) :
                                  theorem Multiset.toFinset_eq_singleton_iff {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) :
                                  Multiset.toFinset s = {a} Multiset.card s 0 s = Multiset.card s {a}
                                  @[simp]
                                  @[simp]
                                  theorem Multiset.toFinset_nonempty {α : Type u_1} [DecidableEq α] {s : Multiset α} :
                                  (Multiset.toFinset s).Nonempty s 0
                                  instance Multiset.isWellFounded_ssubset {β : Type u_2} :
                                  IsWellFounded (Multiset β) fun (x x_1 : Multiset β) => x x_1
                                  Equations
                                  • =
                                  @[simp]
                                  theorem Finset.val_toFinset {α : Type u_1} [DecidableEq α] (s : Finset α) :
                                  theorem Finset.val_le_iff_val_subset {α : Type u_1} {a : Finset α} {b : Multiset α} :
                                  a.val b a.val b
                                  def List.toFinset {α : Type u_1} [DecidableEq α] (l : List α) :

                                  toFinset l removes duplicates from the list l to produce a finset.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem List.toFinset_val {α : Type u_1} [DecidableEq α] (l : List α) :
                                    (List.toFinset l).val = (List.dedup l)
                                    @[simp]
                                    theorem List.toFinset_coe {α : Type u_1} [DecidableEq α] (l : List α) :
                                    theorem List.toFinset_eq {α : Type u_1} [DecidableEq α] {l : List α} (n : List.Nodup l) :
                                    { val := l, nodup := n } = List.toFinset l
                                    @[simp]
                                    theorem List.mem_toFinset {α : Type u_1} [DecidableEq α] {l : List α} {a : α} :
                                    @[simp]
                                    theorem List.coe_toFinset {α : Type u_1} [DecidableEq α] (l : List α) :
                                    (List.toFinset l) = {a : α | a l}
                                    @[simp]
                                    theorem List.toFinset_nil {α : Type u_1} [DecidableEq α] :
                                    @[simp]
                                    theorem List.toFinset_cons {α : Type u_1} [DecidableEq α] {l : List α} {a : α} :
                                    theorem List.toFinset_surj_on {α : Type u_1} [DecidableEq α] :
                                    Set.SurjOn List.toFinset {l : List α | List.Nodup l} Set.univ
                                    theorem List.toFinset.ext_iff {α : Type u_1} [DecidableEq α] {a : List α} {b : List α} :
                                    List.toFinset a = List.toFinset b ∀ (x : α), x a x b
                                    theorem List.toFinset.ext {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} :
                                    (∀ (x : α), x l x l')List.toFinset l = List.toFinset l'
                                    theorem List.toFinset_eq_of_perm {α : Type u_1} [DecidableEq α] (l : List α) (l' : List α) (h : List.Perm l l') :
                                    theorem List.perm_of_nodup_nodup_toFinset_eq {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} (hl : List.Nodup l) (hl' : List.Nodup l') (h : List.toFinset l = List.toFinset l') :
                                    @[simp]
                                    theorem List.toFinset_append {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} :
                                    theorem List.toFinset_replicate_of_ne_zero {α : Type u_1} [DecidableEq α] {a : α} {n : } (hn : n 0) :
                                    @[simp]
                                    theorem List.toFinset_union {α : Type u_1} [DecidableEq α] (l : List α) (l' : List α) :
                                    @[simp]
                                    theorem List.toFinset_inter {α : Type u_1} [DecidableEq α] (l : List α) (l' : List α) :
                                    @[simp]
                                    theorem List.toFinset_eq_empty_iff {α : Type u_1} [DecidableEq α] (l : List α) :
                                    @[simp]
                                    theorem List.toFinset_nonempty_iff {α : Type u_1} [DecidableEq α] (l : List α) :
                                    (List.toFinset l).Nonempty l []
                                    @[simp]
                                    theorem List.toFinset_filter {α : Type u_1} [DecidableEq α] (s : List α) (p : αBool) :
                                    List.toFinset (List.filter p s) = Finset.filter (fun (x : α) => p x = true) (List.toFinset s)
                                    noncomputable def Finset.toList {α : Type u_1} (s : Finset α) :
                                    List α

                                    Produce a list of the elements in the finite set using choice.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Finset.mem_toList {α : Type u_1} {a : α} {s : Finset α} :
                                      @[simp]
                                      theorem Finset.toList_eq_nil {α : Type u_1} {s : Finset α} :
                                      @[simp]
                                      theorem Finset.empty_toList {α : Type u_1} {s : Finset α} :
                                      @[simp]
                                      theorem Finset.toList_empty {α : Type u_1} :
                                      theorem Finset.Nonempty.toList_ne_nil {α : Type u_1} {s : Finset α} (hs : s.Nonempty) :
                                      theorem Finset.Nonempty.not_empty_toList {α : Type u_1} {s : Finset α} (hs : s.Nonempty) :
                                      @[simp]
                                      theorem Finset.coe_toList {α : Type u_1} (s : Finset α) :
                                      (Finset.toList s) = s.val
                                      @[simp]
                                      @[simp]
                                      theorem Finset.toList_eq_singleton_iff {α : Type u_1} {a : α} {s : Finset α} :
                                      Finset.toList s = [a] s = {a}
                                      @[simp]
                                      theorem Finset.toList_singleton {α : Type u_1} (a : α) :
                                      theorem Finset.exists_list_nodup_eq {α : Type u_1} [DecidableEq α] (s : Finset α) :
                                      ∃ (l : List α), List.Nodup l List.toFinset l = s
                                      theorem Finset.toList_cons {α : Type u_1} {a : α} {s : Finset α} (h : as) :
                                      theorem Finset.toList_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : as) :

                                      disjiUnion #

                                      This section is about the bounded union of a disjoint indexed family t : α → Finset β of finite sets over a finite set s : Finset α. In most cases Finset.biUnion should be preferred.

                                      def Finset.disjiUnion {α : Type u_1} {β : Type u_2} (s : Finset α) (t : αFinset β) (hf : Set.PairwiseDisjoint (s) t) :

                                      disjiUnion s f h is the set such that a ∈ disjiUnion s f iff a ∈ f i for some i ∈ s. It is the same as s.biUnion f, but it does not require decidable equality on the type. The hypothesis ensures that the sets are disjoint.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Finset.disjiUnion_val {α : Type u_1} {β : Type u_2} (s : Finset α) (t : αFinset β) (h : Set.PairwiseDisjoint (s) t) :
                                        (Finset.disjiUnion s t h).val = Multiset.bind s.val fun (a : α) => (t a).val
                                        @[simp]
                                        theorem Finset.disjiUnion_empty {α : Type u_1} {β : Type u_2} (t : αFinset β) :
                                        @[simp]
                                        theorem Finset.mem_disjiUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : αFinset β} {b : β} {h : Set.PairwiseDisjoint (s) t} :
                                        b Finset.disjiUnion s t h ∃ a ∈ s, b t a
                                        @[simp]
                                        theorem Finset.coe_disjiUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : αFinset β} {h : Set.PairwiseDisjoint (s) t} :
                                        (Finset.disjiUnion s t h) = ⋃ x ∈ s, (t x)
                                        @[simp]
                                        theorem Finset.disjiUnion_cons {α : Type u_1} {β : Type u_2} (a : α) (s : Finset α) (ha : as) (f : αFinset β) (H : Set.PairwiseDisjoint ((Finset.cons a s ha)) f) :
                                        @[simp]
                                        theorem Finset.singleton_disjiUnion {α : Type u_1} {β : Type u_2} {t : αFinset β} (a : α) {h : Set.PairwiseDisjoint ({a}) t} :
                                        Finset.disjiUnion {a} t h = t a
                                        theorem Finset.disjiUnion_disjiUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Finset α) (f : αFinset β) (g : βFinset γ) (h1 : Set.PairwiseDisjoint (s) f) (h2 : Set.PairwiseDisjoint ((Finset.disjiUnion s f h1)) g) :
                                        Finset.disjiUnion (Finset.disjiUnion s f h1) g h2 = Finset.disjiUnion (Finset.attach s) (fun (a : { x : α // x s }) => Finset.disjiUnion (f a) g )
                                        theorem Finset.disjiUnion_filter_eq_of_maps_to {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : Finset β} {f : αβ} (h : xs, f x t) :
                                        Finset.disjiUnion t (fun (a : β) => Finset.filter (fun (c : α) => f c = a) s) = s

                                        biUnion #

                                        This section is about the bounded union of an indexed family t : α → Finset β of finite sets over a finite set s : Finset α.

                                        def Finset.biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : αFinset β) :

                                        biUnion s t is the union of t x over x ∈ s. (This was formerly bind due to the monad structure on types with DecidableEq.)

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem Finset.biUnion_val {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : αFinset β) :
                                          (Finset.biUnion s t).val = Multiset.dedup (Multiset.bind s.val fun (a : α) => (t a).val)
                                          @[simp]
                                          theorem Finset.biUnion_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] {t : αFinset β} :
                                          @[simp]
                                          theorem Finset.mem_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : αFinset β} {b : β} :
                                          b Finset.biUnion s t ∃ a ∈ s, b t a
                                          @[simp]
                                          theorem Finset.coe_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : αFinset β} :
                                          (Finset.biUnion s t) = ⋃ x ∈ s, (t x)
                                          @[simp]
                                          theorem Finset.biUnion_insert {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : αFinset β} [DecidableEq α] {a : α} :
                                          theorem Finset.biUnion_congr {α : Type u_1} {β : Type u_2} [DecidableEq β] {s₁ : Finset α} {s₂ : Finset α} {t₁ : αFinset β} {t₂ : αFinset β} (hs : s₁ = s₂) (ht : as₁, t₁ a = t₂ a) :
                                          Finset.biUnion s₁ t₁ = Finset.biUnion s₂ t₂
                                          @[simp]
                                          theorem Finset.disjiUnion_eq_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : αFinset β) (hf : Set.PairwiseDisjoint (s) f) :
                                          theorem Finset.biUnion_subset {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : αFinset β} {s' : Finset β} :
                                          Finset.biUnion s t s' xs, t x s'
                                          @[simp]
                                          theorem Finset.singleton_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] {t : αFinset β} {a : α} :
                                          Finset.biUnion {a} t = t a
                                          theorem Finset.biUnion_inter {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : αFinset β) (t : Finset β) :
                                          Finset.biUnion s f t = Finset.biUnion s fun (x : α) => f x t
                                          theorem Finset.inter_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (t : Finset β) (s : Finset α) (f : αFinset β) :
                                          t Finset.biUnion s f = Finset.biUnion s fun (x : α) => t f x
                                          theorem Finset.biUnion_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] (s : Finset α) (f : αFinset β) (g : βFinset γ) :
                                          Finset.biUnion (Finset.biUnion s f) g = Finset.biUnion s fun (a : α) => Finset.biUnion (f a) g
                                          theorem Finset.bind_toFinset {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (s : Multiset α) (t : αMultiset β) :
                                          theorem Finset.biUnion_mono {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t₁ : αFinset β} {t₂ : αFinset β} (h : as, t₁ a t₂ a) :
                                          theorem Finset.biUnion_subset_biUnion_of_subset_left {α : Type u_1} {β : Type u_2} [DecidableEq β] {s₁ : Finset α} {s₂ : Finset α} (t : αFinset β) (h : s₁ s₂) :
                                          theorem Finset.subset_biUnion_of_mem {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (u : αFinset β) {x : α} (xs : x s) :
                                          @[simp]
                                          theorem Finset.biUnion_subset_iff_forall_subset {α : Type u_4} {β : Type u_5} [DecidableEq β] {s : Finset α} {t : Finset β} {f : αFinset β} :
                                          Finset.biUnion s f t xs, f x t
                                          @[simp]
                                          theorem Finset.biUnion_singleton_eq_self {α : Type u_1} {s : Finset α} [DecidableEq α] :
                                          Finset.biUnion s singleton = s
                                          theorem Finset.filter_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : αFinset β) (p : βProp) [DecidablePred p] :
                                          Finset.filter p (Finset.biUnion s f) = Finset.biUnion s fun (a : α) => Finset.filter p (f a)
                                          theorem Finset.biUnion_filter_eq_of_maps_to {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {s : Finset α} {t : Finset β} {f : αβ} (h : xs, f x t) :
                                          (Finset.biUnion t fun (a : β) => Finset.filter (fun (c : α) => f c = a) s) = s
                                          theorem Finset.erase_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : αFinset β) (s : Finset α) (b : β) :
                                          Finset.erase (Finset.biUnion s f) b = Finset.biUnion s fun (x : α) => Finset.erase (f x) b
                                          @[simp]
                                          theorem Finset.biUnion_nonempty {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : αFinset β} :
                                          (Finset.biUnion s t).Nonempty ∃ x ∈ s, (t x).Nonempty
                                          theorem Finset.Nonempty.biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : αFinset β} (hs : s.Nonempty) (ht : xs, (t x).Nonempty) :
                                          (Finset.biUnion s t).Nonempty
                                          theorem Finset.disjoint_biUnion_left {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : αFinset β) (t : Finset β) :
                                          Disjoint (Finset.biUnion s f) t is, Disjoint (f i) t
                                          theorem Finset.disjoint_biUnion_right {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset β) (t : Finset α) (f : αFinset β) :
                                          Disjoint s (Finset.biUnion t f) it, Disjoint s (f i)

                                          choose #

                                          def Finset.chooseX {α : Type u_1} (p : αProp) [DecidablePred p] (l : Finset α) (hp : ∃! (a : α), a l p a) :
                                          { a : α // a l p a }

                                          Given a finset l and a predicate p, associate to a proof that there is a unique element of l satisfying p this unique element, as an element of the corresponding subtype.

                                          Equations
                                          Instances For
                                            def Finset.choose {α : Type u_1} (p : αProp) [DecidablePred p] (l : Finset α) (hp : ∃! (a : α), a l p a) :
                                            α

                                            Given a finset l and a predicate p, associate to a proof that there is a unique element of l satisfying p this unique element, as an element of the ambient type.

                                            Equations
                                            Instances For
                                              theorem Finset.choose_spec {α : Type u_1} (p : αProp) [DecidablePred p] (l : Finset α) (hp : ∃! (a : α), a l p a) :
                                              Finset.choose p l hp l p (Finset.choose p l hp)
                                              theorem Finset.choose_mem {α : Type u_1} (p : αProp) [DecidablePred p] (l : Finset α) (hp : ∃! (a : α), a l p a) :
                                              theorem Finset.choose_property {α : Type u_1} (p : αProp) [DecidablePred p] (l : Finset α) (hp : ∃! (a : α), a l p a) :
                                              p (Finset.choose p l hp)
                                              theorem Finset.pairwise_subtype_iff_pairwise_finset' {α : Type u_1} {β : Type u_2} {s : Finset α} (r : ββProp) (f : αβ) :
                                              Pairwise (r on fun (x : { x : α // x s }) => f x) Set.Pairwise (s) (r on f)
                                              theorem Finset.pairwise_subtype_iff_pairwise_finset {α : Type u_1} {s : Finset α} (r : ααProp) :
                                              Pairwise (r on fun (x : { x : α // x s }) => x) Set.Pairwise (s) r
                                              theorem Finset.pairwise_cons' {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} (ha : as) (r : ββProp) (f : αβ) :
                                              Pairwise (r on fun (a_1 : { x : α // x Finset.cons a s ha }) => f a_1) Pairwise (r on fun (a : { x : α // x s }) => f a) bs, r (f a) (f b) r (f b) (f a)
                                              theorem Finset.pairwise_cons {α : Type u_1} {s : Finset α} {a : α} (ha : as) (r : ααProp) :
                                              Pairwise (r on fun (a_1 : { x : α // x Finset.cons a s ha }) => a_1) Pairwise (r on fun (a : { x : α // x s }) => a) bs, r a b r b a
                                              def Equiv.Finset.union {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (h : Disjoint s t) :
                                              { x : α // x s } { x : α // x t } { x : α // x s t }

                                              The disjoint union of finsets is a sum

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem Equiv.Finset.union_symm_inl {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) (x : { x : α // x s }) :
                                                (Equiv.Finset.union s t h) (Sum.inl x) = { val := x, property := }
                                                @[simp]
                                                theorem Equiv.Finset.union_symm_inr {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) (y : { x : α // x t }) :
                                                (Equiv.Finset.union s t h) (Sum.inr y) = { val := y, property := }
                                                def Equiv.piFinsetUnion {ι : Type u_5} [DecidableEq ι] (α : ιType u_4) {s : Finset ι} {t : Finset ι} (h : Disjoint s t) :
                                                ((i : { x : ι // x s }) → α i) × ((i : { x : ι // x t }) → α i) ((i : { x : ι // x s t }) → α i)

                                                The type of dependent functions on the disjoint union of finsets s ∪ t is equivalent to the type of pairs of functions on s and on t. This is similar to Equiv.sumPiEquivProdPi.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  def Mathlib.Meta.proveFinsetNonempty {u : Lean.Level} {α : Q(Type u)} (s : Q(Finset «$α»)) :
                                                  Lean.MetaM (Option Q(«$s».Nonempty))

                                                  Attempt to prove that a finset is nonempty using the finsetNonempty aesop rule-set.

                                                  You can add lemmas to the rule-set by tagging them with either:

                                                  • aesop safe apply (rule_sets := [finsetNonempty]) if they are always a good idea to follow or
                                                  • aesop unsafe apply (rule_sets := [finsetNonempty]) if they risk directing the search to a blind alley.
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For