Documentation
AddCombi
.
Mathlib
.
Algebra
.
Order
.
GroupWithZero
.
Indicator
Search
return to top
source
Imports
Init
Mathlib.Algebra.Order.ZeroLEOne
AddCombi.Mathlib.Algebra.Notation.Indicator
Mathlib.Algebra.Order.Group.Indicator
Imported by
Set
.
indicator_one_nonneg
Set
.
indicator_one_apply_nonneg
Set
.
indicator_one_pos
source
@[simp]
theorem
Set
.
indicator_one_nonneg
{
α
:
Type
u_1}
{
M
:
Type
u_2}
[
Zero
M
]
[
One
M
]
[
Preorder
M
]
[
ZeroLEOneClass
M
]
{
s
:
Set
α
}
:
0
≤
s
.
indicator
fun (
x
:
α
) =>
1
source
@[simp]
theorem
Set
.
indicator_one_apply_nonneg
{
α
:
Type
u_1}
{
M
:
Type
u_2}
[
Zero
M
]
[
One
M
]
[
Preorder
M
]
[
ZeroLEOneClass
M
]
{
s
:
Set
α
}
{
a
:
α
}
:
0
≤
s
.
indicator
(fun (
x
:
α
) =>
1
)
a
source
@[simp]
theorem
Set
.
indicator_one_pos
{
α
:
Type
u_1}
{
M
:
Type
u_2}
[
Zero
M
]
[
One
M
]
[
PartialOrder
M
]
[
ZeroLEOneClass
M
]
[
NeZero
1
]
{
s
:
Set
α
}
[
Nontrivial
M
]
:
(
0
<
s
.
indicator
fun (
x
:
α
) =>
1
)
↔
s
.
Nonempty