prod_sdiff_eq_prod_sdiff_iff — Mathlib

English

If the images under f are pairwise disjoint and g maps bottom to 1, then the product over the image equals the product over the domain with f applied inside.

Русский

Если образы под f попарно различны и g отображает нижний элемент в 1, то произведение по образу равно произведению по области с применением f внутри.

LaTeX

$$$\\prod_{s \\in I.image f} g(s) = \\prod_{i\\in I} g(f(i))$$$

Lean4

@[to_additive]
theorem prod_sdiff_eq_prod_sdiff_iff : ∏ i ∈ s \ t, f i = ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i = ∏ i ∈ t, f i :=
  eq_comm.trans <|
    eq_iff_eq_of_mul_eq_mul <| by
      rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left, sdiff_union_self_eq_union,
        sdiff_union_self_eq_union, union_comm]

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