Ico_eq_Iio

Mathlib.Data.ENNReal.Operations

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

English

If a ≠ ∞ and b ≤ a, then a − c − (a − b) = b − c for all c.

Русский

Если a ≠ ∞ и b ≤ a, то для любого c выполняется a − c − (a − b) = b − c.

LaTeX

$$$ (ha : a \neq \infty) (h : b \le a) \Rightarrow a - c - (a - b) = b - c $$$

Lean4

protected theorem Ico_eq_Iio : Ico 0 y = Iio y :=
  Ico_bot

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

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

Разделы

Аффилиация

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