multiset_prod_subset_multiset_prod

English

If for every i ∈ t we have f1(i) ⊆ f2(i), then the product over t of f1(i) is a subset of the product over t of f2(i).

Русский

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

LaTeX

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

Lean4

/-- An n-ary version of `Set.mul_subset_mul`. -/
@[to_additive /-- An n-ary version of `Set.add_subset_add`. -/
    ]
theorem multiset_prod_subset_multiset_prod (t : Multiset ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) :
    (t.map f₁).prod ⊆ (t.map f₂).prod :=
  by
  induction t using Quotient.inductionOn
  simp_rw [Multiset.quot_mk_to_coe, Multiset.map_coe, Multiset.prod_coe]
  exact list_prod_subset_list_prod _ _ _ hf

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