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.neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} (hs : Set.Finite s) : Set.Finite (-s)

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

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

theorem Set.Finite.mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : Set.Finite s → Set.Finite t → Set.Finite (s * t)

def Set.fintypeAdd {α : Type u_2} [Add α] [DecidableEq α] (s : Set α) (t : Set α) [Fintype ↑s] [Fintype ↑t] : Fintype ↑(s + t)

Addition preserves finiteness.

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

Multiplication preserves finiteness.

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

theorem Set.decidableMemAdd.proof_1 {α : Type u_1} [AddMonoid α] {s : Set α} {t : Set α} : ∀ (x : α), (∃ x_1 y, x_1 ∈ s ∧ y ∈ t ∧ 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

theorem Set.decidableMemNSMul.proof_1 {α : Type u_1} [AddMonoid α] {s : Set α} : (DecidablePred fun x => x ∈ Nat.zero • s) = DecidablePred fun x => x = 0

theorem Set.decidableMemNSMul.proof_2 {α : Type u_1} [AddMonoid α] {s : Set α} (n : ℕ) : (DecidablePred fun x => x ∈ Nat.succ n • s) = DecidablePred fun x => x ∈ s + n • s

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

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

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

theorem Set.Finite.smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : Set.Finite s → Set.Finite t → Set.Finite (s • t)

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

theorem Set.Finite.smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} : Set.Finite s → Set.Finite (a • s)

theorem Set.Infinite.of_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} : Set.Infinite (a +ᵥ s) → Set.Infinite s

theorem Set.Infinite.of_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} : Set.Infinite (a • s) → Set.Infinite s

theorem Set.Finite.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} (hs : Set.Finite s) (ht : Set.Finite t) : Set.Finite (s -ᵥ t)

theorem Set.infinite_add {α : Type u_2} [Add α] [IsLeftCancelAdd α] [IsRightCancelAdd α] {s : Set α} {t : Set α} : Set.Infinite (s + t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s

theorem Set.infinite_mul {α : Type u_2} [Mul α] [IsLeftCancelMul α] [IsRightCancelMul α] {s : Set α} {t : Set α} : Set.Infinite (s * t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s

@[simp]

theorem Set.finite_vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} {s : Set β} : Set.Finite (a +ᵥ s) ↔ Set.Finite s

@[simp]

theorem Set.finite_smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} {s : Set β} : Set.Finite (a • s) ↔ Set.Finite s

@[simp]

theorem Set.infinite_vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} {s : Set β} : Set.Infinite (a +ᵥ s) ↔ Set.Infinite s

@[simp]

theorem Set.infinite_smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} {s : Set β} : Set.Infinite (a • s) ↔ Set.Infinite s

theorem Set.Finite.of_smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} {s : Set β} : Set.Finite (a • s) → Set.Finite s

Alias of the forward direction of Set.finite_smul_set.

theorem Set.Infinite.smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} {s : Set β} : Set.Infinite s → Set.Infinite (a • s)

Alias of the reverse direction of Set.infinite_smul_set.

theorem Set.Finite.of_vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} {s : Set β} : Set.Finite (a +ᵥ s) → Set.Finite s

theorem Set.Infinite.vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} {s : Set β} : Set.Infinite s → Set.Infinite (a +ᵥ s)

abbrev AddGroup.card_nsmul_eq_card_nsmul_card_univ.match_1 {G : Type u_1} (s : Set G) (motive : ↑s → Sort u_2) : (x : ↑s) → ((b : G) → (hb : b ∈ s) → motive { val := b, property := hb }) → motive x

theorem AddGroup.card_nsmul_eq_card_nsmul_card_univ {G : Type u_5} [AddGroup G] [Fintype G] (S : Set G) [(k : ℕ) → DecidablePred fun x => 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 => x ∈ S ^ k] (k : ℕ) : Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)