English
Equality of intersections with a nonempty set: the intersection of S' interT matches product with singleton arguments.
Русский
Равенство пересечений со множеством непустым: пересечение S'⋂ совпадает с произведением с единичным аргументом.
LaTeX
$$$\bigcap_0 S \times t = \bigcap_{s \in S} (s \times t)$$$
Lean4
theorem sInter_prod {S : Set (Set α)} (hS : S.Nonempty) (t : Set β) : ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t :=
by
rw [← sInter_singleton t, sInter_prod_sInter hS (singleton_nonempty t), sInter_singleton]
simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]