top_mul_top

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.top_mul_top

English

In the extended nonnegative real numbers, the product of infinity with infinity is infinity.

Русский

В расширенных неотрицательных вещественных числах произведение бесконечности на бесконечность равно бесконечности.

LaTeX

$$$\infty \cdot \infty = \infty$$$

Lean4

theorem top_mul_top : ∞ * ∞ = ∞ :=
  WithTop.top_mul_top

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

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

Разделы

Аффилиация

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