English
Under mild nonzero/non-top conditions, (a·b)⁻¹ = a⁻¹·b⁻¹ in ENNReal.
Русский
При умеренных условиях не равенства 0 и бесконечности, в ENNReal выполняется (a·b)⁻¹ = a⁻¹·b⁻¹.
LaTeX
$$$\forall a,b \in \mathbb{R}_{\ge 0}^{\infty},\; (a \neq 0 \lor b \neq \infty) \land (a \neq \infty \lor b \neq 0) \Rightarrow (a b)^{-1} = a^{-1} b^{-1}$$$
Lean4
protected theorem mul_inv {a b : ℝ≥0∞} (ha : a ≠ 0 ∨ b ≠ ∞) (hb : a ≠ ∞ ∨ b ≠ 0) : (a * b)⁻¹ = a⁻¹ * b⁻¹ :=
by
cases b
case top => grind [mul_top, mul_zero, inv_top, ENNReal.inv_eq_zero]
cases a
case top => grind [top_mul, zero_mul, inv_top, ENNReal.inv_eq_zero]
grind [_=_ coe_mul, coe_zero, inv_zero, = mul_inv, coe_ne_top, ENNReal.inv_eq_zero, =_ coe_inv, zero_mul,
= mul_eq_zero, mul_top, mul_zero, top_mul]
