bot_div_of_pos_ne_top

Mathlib.Data.EReal.Inv

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

English

If a > 0 and a ≠ ∞, then 0 / a = 0 or ⊥? (interpreted as ⊥/a = ⊥).

Русский

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

LaTeX

$$$ \bot / a = \bot $$$

Lean4

theorem bot_div_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : ⊥ / a = ⊥ :=
  bot_mul_of_pos (inv_pos_of_pos_ne_top h h')

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

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

Разделы

Аффилиация

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