Finiteness lemmas for pointwise operations on sets

@[simp]

theorem Set.finite_zero {α : Type u_2} [Zero α] : Set.Finite 0

@[simp]

theorem Set.finite_one {α : Type u_2} [One α] : Set.Finite 1

theorem Set.Finite.add {α : Type u_2} [Add α] {s : Set α} {t : Set α} : s.Finite → t.Finite → (s + t).Finite

theorem Set.Finite.mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : s.Finite → t.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

• s.fintypeAdd t = Set.fintypeImage2 (fun (x1 x2 : α) => x1 + x2) s t

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

Multiplication preserves finiteness.

Equations

• s.fintypeMul t = Set.fintypeImage2 (fun (x1 x2 : α) => x1 * x2) s t

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

• Set.decidableMemAdd x = decidable_of_iff (∃ x_1 ∈ s, ∃ y ∈ t, x_1 + y = x) ⋯

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

• Set.decidableMemMul x = decidable_of_iff (∃ x_1 ∈ s, ∃ y ∈ t, x_1 * y = x) ⋯

instance Set.decidableMemNSMul {α : Type u_2} [AddMonoid α] {s : Set α} [Fintype α] [DecidableEq α] [DecidablePred fun (x : α) => x ∈ s] (n : ℕ) : DecidablePred fun (x : α) => x ∈ n • s

Equations

• Set.decidableMemNSMul n = Nat.recAux (⋯.mpr inferInstance) (fun (n : ℕ) (ih : DecidablePred fun (x : α) => x ∈ n • s) => ⋯.mpr inferInstance) n

instance Set.decidableMemPow {α : Type u_2} [Monoid α] {s : Set α} [Fintype α] [DecidableEq α] [DecidablePred fun (x : α) => x ∈ s] (n : ℕ) : DecidablePred fun (x : α) => x ∈ s ^ n

Equations

• Set.decidableMemPow n = Nat.recAux (⋯.mpr inferInstance) (fun (n : ℕ) (ih : DecidablePred fun (x : α) => x ∈ s ^ n) => ⋯.mpr inferInstance) n

theorem Set.Finite.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : s.Finite → t.Finite → (s +ᵥ t).Finite

theorem Set.Finite.smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : s.Finite → t.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).Infinite → s.Infinite

theorem Set.Infinite.of_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} : (a • s).Infinite → s.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⁻¹.Finite → s.Finite

Alias of the forward direction of Set.finite_inv.

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

Alias of the reverse direction of Set.finite_inv.

theorem Set.Finite.of_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} : (-s).Finite → s.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.Finite → t.Finite → (s - t).Finite

theorem Set.Finite.div {α : Type u_2} [Div α] {s : Set α} {t : Set α} : s.Finite → t.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

• s.fintypeSub t = Set.fintypeImage2 (fun (x1 x2 : α) => x1 - x2) s t

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

Division preserves finiteness.

Equations

• s.fintypeDiv t = Set.fintypeImage2 (fun (x1 x2 : α) => x1 / x2) s t

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).Finite → s.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).Finite → s.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 : ℕ) : Fintype.card G ≤ k → Fintype.card ↑(k • S) = Fintype.card ↑(Fintype.card G • S)

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 : ℕ) : Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)