div_pos_iff

Mathlib.Data.ENNReal.Inv

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

English

For ENNReal a,b, 0 < a/b iff a ≠ 0 and b ≠ ∞.

Русский

Для ENNReal чисел a,b: 0 < a/b тогда и только тогда, когда a ≠ 0 и b ≠ ∞.

LaTeX

$$$$ 0 < a/b \iff a \neq 0 \land b \neq \infty. $$$$

Lean4

@[simp]
theorem div_pos_iff : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞ := by simp [pos_iff_ne_zero, not_or]

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

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

Разделы

Аффилиация

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