Documentation

Mathlib.Algebra.Group.Pointwise.Set.Card

Cardinalities of pointwise operations on sets #

source
๐Ÿ“ coverage
theorem Cardinal.mk_mul_le {M : Type u_2} [Mul M] {s t : Set M} :
mk โ†‘(s * t) โ‰ค mk โ†‘s * mk โ†‘t
source
๐Ÿ“ coverage
theorem Cardinal.mk_add_le {M : Type u_2} [Add M] {s t : Set M} :
mk โ†‘(s + t) โ‰ค mk โ†‘s * mk โ†‘t
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
@[simp]
theorem Cardinal.mk_inv {G : Type u_1} [InvolutiveInv G] (s : Set G) :
mk โ†‘sโปยน = mk โ†‘s
source
๐Ÿ“ coverage
@[simp]
theorem Cardinal.mk_neg {G : Type u_1} [InvolutiveNeg G] (s : Set G) :
mk โ†‘(-s) = mk โ†‘s
source
๐Ÿ“ coverage
@[simp]
theorem Set.encard_inv {G : Type u_1} [InvolutiveInv G] (s : Set G) :
sโปยน.encard = s.encard
source
๐Ÿ“ coverage
@[simp]
theorem Set.encard_neg {G : Type u_1} [InvolutiveNeg G] (s : Set G) :
(-s).encard = s.encard
source
๐Ÿ“ coverage
@[simp]
theorem Set.ncard_inv {G : Type u_1} [InvolutiveInv G] (s : Set G) :
sโปยน.ncard = s.ncard
source
๐Ÿ“ coverage
@[simp]
theorem Set.ncard_neg {G : Type u_1} [InvolutiveNeg G] (s : Set G) :
(-s).ncard = s.ncard
source
๐Ÿ“ coverage
theorem Set.natCard_inv {G : Type u_1} [InvolutiveInv G] (s : Set G) :
Nat.card โ†‘sโปยน = Nat.card โ†‘s
source
๐Ÿ“ coverage
theorem Set.natCard_neg {G : Type u_1} [InvolutiveNeg G] (s : Set G) :
Nat.card โ†‘(-s) = Nat.card โ†‘s
source
๐Ÿ“ coverage
theorem Cardinal.mk_div_le {M : Type u_2} [DivInvMonoid M] {s t : Set M} :
mk โ†‘(s / t) โ‰ค mk โ†‘s * mk โ†‘t
source
๐Ÿ“ coverage
theorem Cardinal.mk_sub_le {M : Type u_2} [SubNegMonoid M] {s t : Set M} :
mk โ†‘(s - t) โ‰ค mk โ†‘s * mk โ†‘t
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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