English
If for every a the set t1(a) is contained in t2(a), then the corresponding piFinsets satisfy piFinset t1 ⊆ piFinset t2. Enlarging the coordinate sets cannot shrink the dependent product set.
Русский
Если для каждого a выполнено t1(a) ⊆ t2(a), тогда соответствующие пи-финсеты удовлетворяют piFinset t1 ⊆ piFinset t2. Расширение координат не уменьшает множество зависимого произведения.
LaTeX
$$$\\forall a,\\ t_1(a) \\subseteq t_2(a) \\implies \\operatorname{piFinset} t_1 \\subseteq \\operatorname{piFinset} t_2.$$$
Lean4
theorem piFinset_subset (t₁ t₂ : ∀ a, Finset (δ a)) (h : ∀ a, t₁ a ⊆ t₂ a) : piFinset t₁ ⊆ piFinset t₂ := fun _ hg =>
mem_piFinset.2 fun a => h a <| mem_piFinset.1 hg a
