English
For a finite set s and function f: s → ENNReal with no pair causing a zero and infinity conflict, we have
Русский
Для конечного множества s и функции f: s → ENNReal при отсутствии конфликтов между нулём и бесконечностью выполняется
LaTeX
$$$\left( s \text{ finite},\ \ hf: \text{...} \right) \Rightarrow \left( \prod_{i\in s} f(i) \right)^{-1} = \prod_{i\in s} (f(i))^{-1} \right.$$
Lean4
theorem prod_inv_distrib {ι : Type*} {f : ι → ℝ≥0∞} {s : Finset ι} (hf : s.toSet.Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) :
(∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹ :=
by
induction s using Finset.cons_induction with
| empty => simp
| cons i s hi ih => ?_
simp only [Finset.prod_cons, ← ih (hf.mono <| by simp)]
refine
ENNReal.mul_inv (not_or_of_imp fun hi₀ ↦ prod_ne_top fun j hj ↦ ?_)
(not_or_of_imp fun hi₀ ↦ Finset.prod_ne_zero_iff.2 fun j hj ↦ ?_)
· exact imp_iff_not_or.2 (hf (by simp) (by simp [hj]) <| .symm <| ne_of_mem_of_not_mem hj hi) hi₀
· exact imp_iff_not_or.2 (hf (by simp [hj]) (by simp) <| ne_of_mem_of_not_mem hj hi).symm hi₀
