inv_div — Mathlib

English

In ENNReal, (a/b)⁻¹ = b/a provided non-top/nonzero conditions hold.

Русский

В ENNReal, (a/b)⁻¹ = b/a при соблюдении условий, исключающих ∞ и 0.

LaTeX

$$$\forall a,b \in \mathbb{R}_{\ge 0}^{\infty},\; (b \neq \infty \lor a \neq \infty) \land (b \neq 0 \lor a \neq 0) \Rightarrow (a/b)^{-1} = b/a$$$

Lean4

protected theorem inv_div {a b : ℝ≥0∞} (htop : b ≠ ∞ ∨ a ≠ ∞) (hzero : b ≠ 0 ∨ a ≠ 0) : (a / b)⁻¹ = b / a :=
  by
  rw [← ENNReal.inv_ne_zero] at htop
  rw [← ENNReal.inv_ne_top] at hzero
  rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]

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