Documentation
QuantumInfo
.
ForMathlib
.
Filter
Search
return to top
source
Imports
Init
Mathlib
Mathlib.Tactic.Bound
Imported by
Filter
.
Tendsto_inv_nat_mul_div_real
ENNReal
.
tendsto_toReal_iff_of_eventually_ne_top
source
theorem
Filter
.
Tendsto_inv_nat_mul_div_real
(
m
:
ℕ
)
:
Tendsto
(fun (
x
:
ℕ
) =>
(↑
x
)
⁻¹
*
↑(
x
/
m
)
)
atTop
(
nhds
(
1
/
↑
m
))
source
theorem
ENNReal
.
tendsto_toReal_iff_of_eventually_ne_top
{
ι
:
Type
u_1}
{
fi
:
Filter
ι
}
{
f
:
ι
→
ENNReal
}
(
hf
:
∀ᶠ
(
i
:
ι
)
in
fi
,
f
i
≠
⊤
)
{
x
:
ENNReal
}
(
hx
:
x
≠
⊤
)
:
Filter.Tendsto
(fun (
n
:
ι
) =>
(
f
n
)
.
toReal
)
fi
(
nhds
x
.
toReal
)
↔
Filter.Tendsto
f
fi
(
nhds
x
)