top_div_of_pos_ne_top

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.top_div_of_pos_ne_top

English

If a > 0 and a ≠ ∞, then ∞ / a = ∞.

Русский

Если a > 0 и a ≠ ∞, то ∞ / a = ∞.

LaTeX

$$$ \top / a = \top $$$

Lean4

theorem top_div_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : ⊤ / a = ⊤ :=
  top_mul_of_pos (inv_pos_of_pos_ne_top h h')

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

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

Разделы

Аффилиация

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