piFinset_div — Mathlib

English

For a finite index set ι and families of finite sets s_i, t_i, the division distributes: piFinset (i ↦ s_i / t_i) = piFinset s / piFinset t.

Русский

Для конечного множества индексов ι и семейств конечных множеств s_i и t_i выполняется: piFinset (i ↦ s_i / t_i) = piFinset s / piFinset t.

LaTeX

$$$\\pi\\text{-Finset}(i \\mapsto s_i / t_i) = \\pi\\text{-Finset}(s) / \\pi\\text{-Finset}(t)$$$

Lean4

@[to_additive]
theorem piFinset_div [∀ i, Div (α i)] (s t : ∀ i, Finset (α i)) :
    piFinset (fun i ↦ s i / t i) = piFinset s / piFinset t :=
  piFinset_image₂ _ _ _

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