prod_eraseNone — Mathlib

English

For f : α → M and s : Finset (Option α),

Русский

Пусть f : α → M и s : Finset (Option α)

LaTeX

$$$$ \\prod_{x ∈ \\mathrm{eraseNone}(s)} f(x) = \\prod_{x ∈ s} \\mathrm{Option.elim'}(1) f(x). $$$$

Lean4

@[to_additive]
theorem prod_eraseNone (f : α → M) (s : Finset (Option α)) : ∏ x ∈ eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x := by
  classical
    calc
    ∏ x ∈ eraseNone s, f x = ∏ x ∈ (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
      (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
    _ = ∏ x ∈ s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
    _ = ∏ x ∈ s, Option.elim' 1 f x := prod_erase _ rfl

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