mem_Iio_self_add

Mathlib.Data.ENNReal.Operations

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

English

If x ≠ ∞ and ε ≠ 0, then x ∈ Iio (x + ε).

Русский

Если x ≠ ∞ и ε ≠ 0, то x ∈ Iio(x + ε).

LaTeX

$$$ x \neq \infty \Rightarrow \epsilon \neq 0 \Rightarrow x \in Iio (x + \epsilon) $$$

Lean4

theorem mem_Iio_self_add : x ≠ ∞ → ε ≠ 0 → x ∈ Iio (x + ε) := fun xt ε0 => lt_add_right xt ε0

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

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

Разделы

Аффилиация

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