tendsto_toNNReal_atTop

Mathlib.Topology.Instances.NNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#Real.tendsto_toNNReal_atTop

English

Tendsto Real.toNNReal atTop atTop; (alternative form).

Русский

Сходимость Real.toNNReal при atTop в atTop (альтернативная форма).

LaTeX

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

Lean4

theorem _root_.Real.tendsto_toNNReal_atTop : Tendsto Real.toNNReal atTop atTop :=
  Real.tendsto_toNNReal_atTop_iff.2 tendsto_id

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

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

Разделы

Аффилиация

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