listProd_mem — Mathlib

English

If there exists x ∈ l with f(x) ∈ I, then the product of the mapped elements lies in I.

Русский

Если существует x ∈ l с f(x) ∈ I, то произведение отображённых элементов лежит в I.

LaTeX

$$∃ x ∈ l, f x ∈ I ⇒ (l.map f).prod ∈ I$$

Lean4

theorem listProd_mem {ι : Type*} (l : List ι) (f : ι → R) (hl : ∃ x ∈ l, f x ∈ I) : (l.map f).prod ∈ I := by
  induction l with
  | nil => simp only [List.not_mem_nil, false_and, exists_false] at hl
  | cons x l ih =>
    simp only [List.mem_cons, exists_eq_or_imp] at hl
    rcases hl with h | hal
    · simpa only [List.map_cons, List.prod_cons] using I.mul_mem_right _ _ h
    · simpa only [List.map_cons, List.prod_cons] using I.mul_mem_left _ _ <| ih hal

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