Documentation

Mathlib.Data.Set.Pointwise.Finite

Finiteness lemmas for pointwise operations on sets #

@[simp]
theorem Set.finite_zero {α : Type u_2} [Zero α] :
@[simp]
theorem Set.finite_one {α : Type u_2} [One α] :
theorem Set.Finite.add {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
s.Finitet.Finite(s + t).Finite
theorem Set.Finite.mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
s.Finitet.Finite(s * t).Finite
def Set.fintypeAdd {α : Type u_2} [Add α] [DecidableEq α] (s : Set α) (t : Set α) [Fintype s] [Fintype t] :
Fintype (s + t)

Addition preserves finiteness.

Equations
Instances For
    def Set.fintypeMul {α : Type u_2} [Mul α] [DecidableEq α] (s : Set α) (t : Set α) [Fintype s] [Fintype t] :
    Fintype (s * t)

    Multiplication preserves finiteness.

    Equations
    Instances For
      instance Set.decidableMemAdd {α : Type u_2} [AddMonoid α] {s : Set α} {t : Set α} [Fintype α] [DecidableEq α] [DecidablePred fun (x : α) => x s] [DecidablePred fun (x : α) => x t] :
      DecidablePred fun (x : α) => x s + t
      Equations
      theorem Set.decidableMemAdd.proof_1 {α : Type u_1} [AddMonoid α] {s : Set α} {t : Set α} :
      ∀ (x : α), (∃ x_1s, yt, x_1 + y = x) x s + t
      instance Set.decidableMemMul {α : Type u_2} [Monoid α] {s : Set α} {t : Set α} [Fintype α] [DecidableEq α] [DecidablePred fun (x : α) => x s] [DecidablePred fun (x : α) => x t] :
      DecidablePred fun (x : α) => x s * t
      Equations
      instance Set.decidableMemNSMul {α : Type u_2} [AddMonoid α] {s : Set α} [Fintype α] [DecidableEq α] [DecidablePred fun (x : α) => x s] (n : ) :
      DecidablePred fun (x : α) => x n s
      Equations
      theorem Set.decidableMemNSMul.proof_2 {α : Type u_1} [AddMonoid α] {s : Set α} (n : ) :
      (DecidablePred fun (x : α) => x (n + 1) s) = DecidablePred fun (x : α) => x n s + s
      theorem Set.decidableMemNSMul.proof_1 {α : Type u_1} [AddMonoid α] {s : Set α} :
      (DecidablePred fun (x : α) => x 0 s) = DecidablePred fun (x : α) => x = 0
      instance Set.decidableMemPow {α : Type u_2} [Monoid α] {s : Set α} [Fintype α] [DecidableEq α] [DecidablePred fun (x : α) => x s] (n : ) :
      DecidablePred fun (x : α) => x s ^ n
      Equations
      theorem Set.Finite.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
      s.Finitet.Finite(s +ᵥ t).Finite
      theorem Set.Finite.smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
      s.Finitet.Finite(s t).Finite
      theorem Set.Finite.vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} :
      s.Finite(a +ᵥ s).Finite
      theorem Set.Finite.smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} :
      s.Finite(a s).Finite
      theorem Set.Infinite.of_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} :
      (a +ᵥ s).Infinites.Infinite
      theorem Set.Infinite.of_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} :
      (a s).Infinites.Infinite
      theorem Set.Finite.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
      (s -ᵥ t).Finite
      theorem Set.finite_add {α : Type u_2} [Add α] [IsLeftCancelAdd α] [IsRightCancelAdd α] {s : Set α} {t : Set α} :
      (s + t).Finite s.Finite t.Finite s = t =
      theorem Set.finite_mul {α : Type u_2} [Mul α] [IsLeftCancelMul α] [IsRightCancelMul α] {s : Set α} {t : Set α} :
      (s * t).Finite s.Finite t.Finite s = t =
      theorem Set.infinite_add {α : Type u_2} [Add α] [IsLeftCancelAdd α] [IsRightCancelAdd α] {s : Set α} {t : Set α} :
      (s + t).Infinite s.Infinite t.Nonempty t.Infinite s.Nonempty
      theorem Set.infinite_mul {α : Type u_2} [Mul α] [IsLeftCancelMul α] [IsRightCancelMul α] {s : Set α} {t : Set α} :
      (s * t).Infinite s.Infinite t.Nonempty t.Infinite s.Nonempty
      @[simp]
      theorem Set.finite_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
      (-s).Finite s.Finite
      @[simp]
      theorem Set.finite_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :
      s⁻¹.Finite s.Finite
      @[simp]
      theorem Set.infinite_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
      (-s).Infinite s.Infinite
      @[simp]
      theorem Set.infinite_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :
      s⁻¹.Infinite s.Infinite
      theorem Set.Finite.of_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :
      s⁻¹.Finites.Finite

      Alias of the forward direction of Set.finite_inv.

      theorem Set.Finite.inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :
      s.Finites⁻¹.Finite

      Alias of the reverse direction of Set.finite_inv.

      theorem Set.Finite.of_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
      (-s).Finites.Finite
      theorem Set.Finite.neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
      s.Finite(-s).Finite
      theorem Set.Finite.sub {α : Type u_2} [Sub α] {s : Set α} {t : Set α} :
      s.Finitet.Finite(s - t).Finite
      theorem Set.Finite.div {α : Type u_2} [Div α] {s : Set α} {t : Set α} :
      s.Finitet.Finite(s / t).Finite
      def Set.fintypeSub {α : Type u_2} [Sub α] [DecidableEq α] (s : Set α) (t : Set α) [Fintype s] [Fintype t] :
      Fintype (s - t)

      Subtraction preserves finiteness.

      Equations
      Instances For
        def Set.fintypeDiv {α : Type u_2} [Div α] [DecidableEq α] (s : Set α) (t : Set α) [Fintype s] [Fintype t] :
        Fintype (s / t)

        Division preserves finiteness.

        Equations
        Instances For
          theorem Set.finite_sub {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} :
          (s - t).Finite s.Finite t.Finite s = t =
          theorem Set.finite_div {α : Type u_2} [Group α] {s : Set α} {t : Set α} :
          (s / t).Finite s.Finite t.Finite s = t =
          theorem Set.infinite_sub {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} :
          (s - t).Infinite s.Infinite t.Nonempty t.Infinite s.Nonempty
          theorem Set.infinite_div {α : Type u_2} [Group α] {s : Set α} {t : Set α} :
          (s / t).Infinite s.Infinite t.Nonempty t.Infinite s.Nonempty
          @[simp]
          theorem Set.finite_vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} {s : Set β} :
          (a +ᵥ s).Finite s.Finite
          @[simp]
          theorem Set.finite_smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} {s : Set β} :
          (a s).Finite s.Finite
          @[simp]
          theorem Set.infinite_vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} {s : Set β} :
          (a +ᵥ s).Infinite s.Infinite
          @[simp]
          theorem Set.infinite_smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} {s : Set β} :
          (a s).Infinite s.Infinite
          theorem Set.Finite.of_smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} {s : Set β} :
          (a s).Finites.Finite

          Alias of the forward direction of Set.finite_smul_set.

          theorem Set.Finite.of_vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} {s : Set β} :
          (a +ᵥ s).Finites.Finite
          theorem Set.Infinite.smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} {s : Set β} :
          s.Infinite(a s).Infinite

          Alias of the reverse direction of Set.infinite_smul_set.

          theorem Set.Infinite.vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} {s : Set β} :
          s.Infinite(a +ᵥ s).Infinite
          theorem AddGroup.card_nsmul_eq_card_nsmul_card_univ {G : Type u_5} [AddGroup G] [Fintype G] (S : Set G) [(k : ) → DecidablePred fun (x : G) => x k S] (k : ) :
          theorem Group.card_pow_eq_card_pow_card_univ {G : Type u_5} [Group G] [Fintype G] (S : Set G) [(k : ) → DecidablePred fun (x : G) => x S ^ k] (k : ) :