HepLean Documentation

Mathlib.Algebra.Group.Pointwise.Set.Card

Cardinalities of pointwise operations on sets #

source
theorem Cardinal.mk_mul_le {M : Type u_2} [Mul M] {s t : Set M} :
Cardinal.mk ↑(s * t) ≤ Cardinal.mk ↑s * Cardinal.mk ↑t
source
theorem Cardinal.mk_add_le {M : Type u_2} [Add M] {s t : Set M} :
Cardinal.mk ↑(s + t) ≤ Cardinal.mk ↑s * Cardinal.mk ↑t
source
theorem Set.natCard_mul_le {M : Type u_2} [Mul M] {s t : Set M} [IsCancelMul M] :
Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t
source
theorem Set.natCard_add_le {M : Type u_2} [Add M] {s t : Set M} [IsCancelAdd M] :
Nat.card ↑(s + t) ≤ Nat.card ↑s * Nat.card ↑t
source
@[deprecated Set.natCard_mul_le]
theorem Set.card_mul_le {M : Type u_2} [Mul M] {s t : Set M} [IsCancelMul M] :
Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

Alias of Set.natCard_mul_le.

source
@[deprecated Set.natCard_add_le]
theorem Set.card_add_le {M : Type u_2} [Add M] {s t : Set M} [IsCancelAdd M] :
Nat.card ↑(s + t) ≤ Nat.card ↑s * Nat.card ↑t
source
@[simp]
theorem Cardinal.mk_inv {G : Type u_1} [InvolutiveInv G] (s : Set G) :
Cardinal.mk ↑s⁻¹ = Cardinal.mk ↑s
source
@[simp]
theorem Cardinal.mk_neg {G : Type u_1} [InvolutiveNeg G] (s : Set G) :
Cardinal.mk ↑(-s) = Cardinal.mk ↑s
source
@[simp]
theorem Set.natCard_inv {G : Type u_1} [InvolutiveInv G] (s : Set G) :
Nat.card ↑s⁻¹ = Nat.card ↑s
source
@[simp]
theorem Set.natCard_neg {G : Type u_1} [InvolutiveNeg G] (s : Set G) :
Nat.card ↑(-s) = Nat.card ↑s
source
@[deprecated Set.natCard_inv]
theorem Set.card_inv {G : Type u_1} [InvolutiveInv G] (s : Set G) :
Nat.card ↑s⁻¹ = Nat.card ↑s

Alias of Set.natCard_inv.

source
@[deprecated Set.natCard_neg]
theorem Set.card_neg {G : Type u_1} [InvolutiveNeg G] (s : Set G) :
Nat.card ↑(-s) = Nat.card ↑s
source
@[simp]
theorem Set.encard_inv {G : Type u_1} [InvolutiveInv G] (s : Set G) :
s⁻¹.encard = s.encard
source
@[simp]
theorem Set.encard_neg {G : Type u_1} [InvolutiveNeg G] (s : Set G) :
(-s).encard = s.encard
source
@[simp]
theorem Set.ncard_inv {G : Type u_1} [InvolutiveInv G] (s : Set G) :
s⁻¹.ncard = s.ncard
source
@[simp]
theorem Set.ncard_neg {G : Type u_1} [InvolutiveNeg G] (s : Set G) :
(-s).ncard = s.ncard
source
theorem Cardinal.mk_div_le {M : Type u_2} [DivInvMonoid M] {s t : Set M} :
Cardinal.mk ↑(s / t) ≤ Cardinal.mk ↑s * Cardinal.mk ↑t
source
theorem Cardinal.mk_sub_le {M : Type u_2} [SubNegMonoid M] {s t : Set M} :
Cardinal.mk ↑(s - t) ≤ Cardinal.mk ↑s * Cardinal.mk ↑t
source
theorem Set.natCard_div_le {G : Type u_1} [Group G] {s t : Set G} :
Nat.card ↑(s / t) ≤ Nat.card ↑s * Nat.card ↑t
source
theorem Set.natCard_sub_le {G : Type u_1} [AddGroup G] {s t : Set G} :
Nat.card ↑(s - t) ≤ Nat.card ↑s * Nat.card ↑t
source
@[deprecated Set.natCard_div_le]
theorem Set.card_div_le {G : Type u_1} [Group G] {s t : Set G} :
Nat.card ↑(s / t) ≤ Nat.card ↑s * Nat.card ↑t

Alias of Set.natCard_div_le.

source
@[deprecated Set.natCard_sub_le]
theorem Set.card_sub_le {G : Type u_1} [AddGroup G] {s t : Set G} :
Nat.card ↑(s - t) ≤ Nat.card ↑s * Nat.card ↑t
source
@[simp]
theorem Cardinal.mk_smul_set {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] (a : G) (s : Set α) :
Cardinal.mk ↑(a • s) = Cardinal.mk ↑s
source
@[simp]
theorem Cardinal.mk_vadd_set {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] (a : G) (s : Set α) :
Cardinal.mk ↑(a +ᵥ s) = Cardinal.mk ↑s
source
@[simp]
theorem Set.natCard_smul_set {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] (a : G) (s : Set α) :
Nat.card ↑(a • s) = Nat.card ↑s
source
@[simp]
theorem Set.natCard_vadd_set {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] (a : G) (s : Set α) :
Nat.card ↑(a +ᵥ s) = Nat.card ↑s
source
@[deprecated Cardinal.mk_smul_set]
theorem Set.card_smul_set {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] (a : G) (s : Set α) :
Cardinal.mk ↑(a • s) = Cardinal.mk ↑s

Alias of Cardinal.mk_smul_set.

source
@[deprecated Cardinal.mk_vadd_set]
theorem Set.card_vadd_set {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] (a : G) (s : Set α) :
Cardinal.mk ↑(a +ᵥ s) = Cardinal.mk ↑s
source
@[simp]
theorem Set.encard_smul_set {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] (a : G) (s : Set α) :
(a • s).encard = s.encard
source
@[simp]
theorem Set.encard_vadd_set {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] (a : G) (s : Set α) :
(a +ᵥ s).encard = s.encard
source
@[simp]
theorem Set.ncard_smul_set {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] (a : G) (s : Set α) :
(a • s).ncard = s.ncard
source
@[simp]
theorem Set.ncard_vadd_set {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] (a : G) (s : Set α) :
(a +ᵥ s).ncard = s.ncard