sInter_prod_sInter_subset — Mathlib

English

The product of intersections contains the intersection over the cross product of the families: ⋂ S ×ˢ ⋂ T ⊆ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2.

Русский

Произведение пересечений содержится в пересечении попарных произведений; представленное как подмножество.

LaTeX

$$$\bigcap S \times\!\bigcap T \subseteq \bigcap_{r \in S \times T} (r_1 \times r_2)$$$

Lean4

theorem sInter_prod_sInter_subset (S : Set (Set α)) (T : Set (Set β)) : ⋂₀ S ×ˢ ⋂₀ T ⊆ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2 :=
  subset_iInter₂ fun x hx _ hy => ⟨hy.1 x.1 hx.1, hy.2 x.2 hx.2⟩

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