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} :
mk ↑(s * t) ≤ mk ↑s * mk ↑t
source
theorem Cardinal.mk_add_le {M : Type u_2} [Add M] {s t : Set M} :
mk ↑(s + t) ≤ mk ↑s * 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
@[simp]
theorem Cardinal.mk_inv {G : Type u_1} [InvolutiveInv G] (s : Set G) :
mk ↑s⁻¹ = mk ↑s
source
@[simp]
theorem Cardinal.mk_neg {G : Type u_1} [InvolutiveNeg G] (s : Set G) :
mk ↑(-s) = 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
@[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} :
mk ↑(s / t) ≤ mk ↑s * mk ↑t
source
theorem Cardinal.mk_sub_le {M : Type u_2} [SubNegMonoid M] {s t : Set M} :
mk ↑(s - t) ≤ mk ↑s * 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
@[simp]
theorem Cardinal.mk_smul_set {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] (a : G) (s : Set α) :
mk ↑(a • s) = mk ↑s
source
@[simp]
theorem Cardinal.mk_vadd_set {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] (a : G) (s : Set α) :
mk ↑(a +ᵥ s) = 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
@[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