piFinset_inv — Mathlib

English

For a finite index set ι and families of sets α_i with inverses, the piFinset of inverses equals the inverse of the piFinset: piFinset (i ↦ (s_i)⁻¹) = (piFinset s)⁻¹.

Русский

Для конечного множества индексов ι и семейств множеств s_i с обратимыми элементами выполняется: piFinset (i ↦ s_i)⁻¹ = piFinset (i ↦ s_i⁻¹).

LaTeX

$$$\\pi\\text{-Finset}(i \\mapsto s_i^{-1}) = (\\pi\\text{-Finset}(s_i))^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem piFinset_inv [∀ i, Inv (α i)] (s : ∀ i, Finset (α i)) : piFinset (fun i ↦ (s i)⁻¹) = (piFinset s)⁻¹ :=
  piFinset_image _ _

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