list_prod_subset_list_prod — Mathlib

English

If for each i in the list t we have f1(i) ⊆ f2(i), then the list-product (t.map f1).prod is a subset of (t.map f2).prod.

Русский

Если для каждого i из списка t выполняется f1(i) ⊆ f2(i), то их списковое произведение принадлежит произведению f2.

LaTeX

$$(t.map f1).prod ⊆ (t.map f2).prod$$

Lean4

/-- An n-ary version of `Set.mul_subset_mul`. -/
@[to_additive /-- An n-ary version of `Set.add_subset_add`. -/
    ]
theorem list_prod_subset_list_prod (t : List ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) :
    (t.map f₁).prod ⊆ (t.map f₂).prod := by
  induction t with
  | nil => rfl
  | cons h tl ih =>
    simp_rw [List.map_cons, List.prod_cons]
    exact mul_subset_mul (hf h List.mem_cons_self) (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)

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