pi_subset — Mathlib

English

If t1(a) ⊆ t2(a) for all a ∈ s, then s.pi t1 ⊆ s.pi t2.

Русский

Если t1(a) ⊆ t2(a) для всех a ∈ s, тогда s.pi t1 ⊆ s.pi t2.

LaTeX

$$$ s.\\pi t_1 \\subseteq s.\\pi t_2 \\quad \\text{whenever } \\forall a \\in s, t_1(a) \\subseteq t_2(a). $$$

Lean4

theorem pi_subset {s : Finset α} (t₁ t₂ : ∀ a, Finset (β a)) (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) : s.pi t₁ ⊆ s.pi t₂ :=
  fun _ hg => mem_pi.2 fun a ha => h a ha (mem_pi.mp hg a ha)

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