tendsto_real_toNNReal_atTop

Mathlib.Topology.Instances.NNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#tendsto_real_toNNReal_atTop

English

Tendsto Real.toNNReal atTop atTop; equivalently, tendsto_iff holds with atTop.

Русский

Сходимость Real.toNNReal при atTop к atTop; эквивалентно условию предиката.

LaTeX

$$$\\text{tendsto\_real\_toNNReal\_atTop\_iff}$$$

Lean4

theorem _root_.tendsto_real_toNNReal_atTop : Tendsto Real.toNNReal atTop atTop :=
  Real.map_toNNReal_atTop.le

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru