Documentation
AddCombi
.
Mathlib
.
Data
.
Finset
.
Density
Search
return to top
source
Imports
Init
Mathlib.Data.Finset.Density
Mathlib.Data.Fintype.Prod
AddCombi.Mathlib.Data.NNRat.Order
Imported by
Finset
.
dens_product
Finset
.
dens_union_eq_dens_add_dens
Finset
.
dens_sdiff_of_subset
Finset
.
cast_dens_inter
Finset
.
cast_dens_union
Finset
.
cast_dens_sdiff
source
@[simp]
theorem
Finset
.
dens_product
{
α
:
Type
u_2}
{
β
:
Type
u_3}
[
Fintype
α
]
[
Fintype
β
]
(
s
:
Finset
α
)
(
t
:
Finset
β
)
:
(
s
×ˢ
t
).
dens
=
s
.
dens
*
t
.
dens
source
theorem
Finset
.
dens_union_eq_dens_add_dens
{
α
:
Type
u_2}
[
Fintype
α
]
{
s
t
:
Finset
α
}
[
DecidableEq
α
]
:
(
s
∪
t
).
dens
=
s
.
dens
+
t
.
dens
↔
Disjoint
s
t
source
theorem
Finset
.
dens_sdiff_of_subset
{
α
:
Type
u_2}
[
Fintype
α
]
{
s
t
:
Finset
α
}
[
DecidableEq
α
]
(
h
:
s
⊆
t
)
:
(
t
\
s
).
dens
=
t
.
dens
-
s
.
dens
source
theorem
Finset
.
cast_dens_inter
{
K
:
Type
u_1}
{
α
:
Type
u_2}
[
DivisionRing
K
]
[
CharZero
K
]
[
Fintype
α
]
{
s
t
:
Finset
α
}
[
DecidableEq
α
]
:
↑
(
s
∩
t
).
dens
=
↑
s
.
dens
+
↑
t
.
dens
-
↑
(
s
∪
t
).
dens
source
theorem
Finset
.
cast_dens_union
{
K
:
Type
u_1}
{
α
:
Type
u_2}
[
DivisionRing
K
]
[
CharZero
K
]
[
Fintype
α
]
{
s
t
:
Finset
α
}
[
DecidableEq
α
]
:
↑
(
s
∪
t
).
dens
=
↑
s
.
dens
+
↑
t
.
dens
-
↑
(
s
∩
t
).
dens
source
theorem
Finset
.
cast_dens_sdiff
{
K
:
Type
u_1}
{
α
:
Type
u_2}
[
DivisionRing
K
]
[
CharZero
K
]
[
Fintype
α
]
{
s
t
:
Finset
α
}
[
DecidableEq
α
]
(
h
:
s
⊆
t
)
:
↑
(
t
\
s
).
dens
=
↑
t
.
dens
-
↑
s
.
dens