finset_prod_subset_finset_prod — Mathlib

English

If each f1 i ⊆ f2 i for i in t, then ∏ i∈t f1 i ⊆ ∏ i∈t f2 i.

Русский

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

LaTeX

$$∏ i ∈ t, f1 i ⊆ ∏ i ∈ t, f2 i$$

Lean4

/-- An n-ary version of `Set.mul_subset_mul`. -/
@[to_additive /-- An n-ary version of `Set.add_subset_add`. -/
    ]
theorem finset_prod_subset_finset_prod (t : Finset ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) :
    ∏ i ∈ t, f₁ i ⊆ ∏ i ∈ t, f₂ i :=
  multiset_prod_subset_multiset_prod _ _ _ hf

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