Documentation
FormalConjectures
.
ForMathlib
.
Algebra
.
Order
.
Group
.
Pointwise
.
Interval
Search
return to top
source
Imports
Init
Mathlib.Tactic
Mathlib.Algebra.Order.Group.Pointwise.Interval
Imported by
Nat
.
image_mul_two_Iio_even
Nat
.
image_mul_two_Iio
source
theorem
Nat
.
image_mul_two_Iio_even
{n :
ℕ
}
(h :
Even
n
)
:
(fun (
x
:
ℕ
) =>
2
*
x
)
''
Set.Iio
(
n
/
2
)
=
{
n
:
ℕ
|
Even
n
}
∩
Set.Iio
n
source
theorem
Nat
.
image_mul_two_Iio
(n :
ℕ
)
:
(fun (
x
:
ℕ
) =>
2
*
x
)
''
Set.Iio
((
n
+
1
)
/
2
)
=
{
n
:
ℕ
|
Even
n
}
∩
Set.Iio
n