finset_prod — Mathlib

English

Let M be a commutative monoid. For a finite nonempty index set s ⊆ ℕ, the Finset product ∏ i∈s a.get i lies in FP a.

Русский

Пусть M — коммутативный моноид. Для конечного непустого множества индексов s ⊆ ℕ произведение ∏_{i ∈ s} a.get i принадлежит FP a.

LaTeX

$$$$ \forall {M} [CommMonoid M] (a : Stream' M) (s : Finset \mathbb{N}) (hs : s.Nonempty), (s.prod (\lambda i, a.get i)) \in FP a $$$$

Lean4

@[to_additive]
theorem finset_prod {M} [CommMonoid M] (a : Stream' M) (s : Finset ℕ) (hs : s.Nonempty) :
    (s.prod fun i => a.get i) ∈ FP a :=
  by
  refine FP_drop_subset_FP _ (s.min' hs) ?_
  induction s using Finset.eraseInduction with
  | H s ih => _
  rw [← Finset.mul_prod_erase _ _ (s.min'_mem hs), ← Stream'.head_drop]
  rcases (s.erase (s.min' hs)).eq_empty_or_nonempty with h | h
  · rw [h, Finset.prod_empty, mul_one]
    exact FP.head _
  · apply FP.cons
    rw [Stream'.tail_eq_drop, Stream'.drop_drop, add_comm]
    refine Set.mem_of_subset_of_mem ?_ (ih _ (s.min'_mem hs) h)
    have : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h :=
      Nat.succ_le_of_lt (Finset.min'_lt_of_mem_erase_min' _ _ <| Finset.min'_mem _ _)
    obtain ⟨d, hd⟩ := Nat.exists_eq_add_of_le this
    rw [hd, ← Stream'.drop_drop, add_comm]
    apply FP_drop_subset_FP

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