div_pos

Mathlib.Data.EReal.Inv

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

English

If 0 < a, 0 < b and b ≠ ⊤, then 0 < a / b.

Русский

Если 0 < a, 0 < b и b ≠ ⊤, то 0 < a / b.

LaTeX

$$$0 < a \land 0 < b \land b \neq \top \Rightarrow 0 < a / b$$$

Lean4

theorem div_pos (ha : 0 < a) (hb : 0 < b) (hb' : b ≠ ⊤) : 0 < a / b :=
  EReal.mul_pos ha (inv_pos_of_pos_ne_top hb hb')

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

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

Разделы

Аффилиация

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