Cardinalities of pointwise operations on sets.

@[simp]

theorem Set.card_vadd_set {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (a : α) (s : Set β) : Nat.card ↑(a +ᵥ s) = Nat.card ↑s

@[simp]

theorem Set.card_smul_set {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (a : α) (s : Set β) : Nat.card ↑(a • s) = Nat.card ↑s

theorem Set.card_add_le {α : Type u_1} [Add α] [IsCancelAdd α] {s : Set α} {t : Set α} : Nat.card ↑(s + t) ≤ Nat.card ↑s * Nat.card ↑t

theorem Set.card_mul_le {α : Type u_1} [Mul α] [IsCancelMul α] {s : Set α} {t : Set α} : Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

@[simp]

theorem Set.card_neg {α : Type u_1} [InvolutiveNeg α] (s : Set α) : Nat.card ↑(-s) = Nat.card ↑s

@[simp]

theorem Set.card_inv {α : Type u_1} [InvolutiveInv α] (s : Set α) : Nat.card ↑s⁻¹ = Nat.card ↑s

theorem Set.card_sub_le {α : Type u_1} [AddGroup α] {s : Set α} {t : Set α} : Nat.card ↑(s - t) ≤ Nat.card ↑s * Nat.card ↑t

theorem Set.card_div_le {α : Type u_1} [Group α] {s : Set α} {t : Set α} : Nat.card ↑(s / t) ≤ Nat.card ↑s * Nat.card ↑t