Documentation
Mathlib
.
Algebra
.
Group
.
Pointwise
.
Set
.
Card
Search
Google site search
return to top
source
Imports
Init
Mathlib.SetTheory.Cardinal.Finite
Mathlib.Algebra.Group.Pointwise.Finset.Basic
Imported by
Set
.
card_vadd_set
Set
.
card_smul_set
Set
.
card_add_le
Set
.
card_mul_le
Set
.
card_neg
Set
.
card_inv
Set
.
card_sub_le
Set
.
card_div_le
Cardinalities of pointwise operations on sets.
#
source
@[simp]
theorem
Set
.
card_vadd_set
{α :
Type
u_1}
{β :
Type
u_2}
[
AddGroup
α
]
[
AddAction
α
β
]
(a :
α
)
(s :
Set
β
)
:
Nat.card
↑
(
a
+ᵥ
s
)
=
Nat.card
↑
s
source
@[simp]
theorem
Set
.
card_smul_set
{α :
Type
u_1}
{β :
Type
u_2}
[
Group
α
]
[
MulAction
α
β
]
(a :
α
)
(s :
Set
β
)
:
Nat.card
↑
(
a
•
s
)
=
Nat.card
↑
s
source
theorem
Set
.
card_add_le
{α :
Type
u_1}
[
Add
α
]
[
IsCancelAdd
α
]
{s :
Set
α
}
{t :
Set
α
}
:
Nat.card
↑
(
s
+
t
)
≤
Nat.card
↑
s
*
Nat.card
↑
t
source
theorem
Set
.
card_mul_le
{α :
Type
u_1}
[
Mul
α
]
[
IsCancelMul
α
]
{s :
Set
α
}
{t :
Set
α
}
:
Nat.card
↑
(
s
*
t
)
≤
Nat.card
↑
s
*
Nat.card
↑
t
source
@[simp]
theorem
Set
.
card_neg
{α :
Type
u_1}
[
InvolutiveNeg
α
]
(s :
Set
α
)
:
Nat.card
↑
(
-
s
)
=
Nat.card
↑
s
source
@[simp]
theorem
Set
.
card_inv
{α :
Type
u_1}
[
InvolutiveInv
α
]
(s :
Set
α
)
:
Nat.card
↑
s
⁻¹
=
Nat.card
↑
s
source
theorem
Set
.
card_sub_le
{α :
Type
u_1}
[
AddGroup
α
]
{s :
Set
α
}
{t :
Set
α
}
:
Nat.card
↑
(
s
-
t
)
≤
Nat.card
↑
s
*
Nat.card
↑
t
source
theorem
Set
.
card_div_le
{α :
Type
u_1}
[
Group
α
]
{s :
Set
α
}
{t :
Set
α
}
:
Nat.card
↑
(
s
/
t
)
≤
Nat.card
↑
s
*
Nat.card
↑
t