div_pos

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

If a > 0 and b > 0, then a/b > 0 (divisive positivity).

Русский

Если a > 0 и b > 0, то a/b > 0 (положительность частного).

LaTeX

$$$\forall a,b\; (0 < a) \land (0 < b) \Rightarrow 0 < a/b$$$

Lean4

theorem div_pos (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by rw [div_eq_mul_inv]; exact mul_pos ha (inv_pos.2 hb)

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

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

Разделы

Аффилиация

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