Documentation

Mathlib.Algebra.Group.Pointwise.Set.Card

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 α) :
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