sInter_prod — Mathlib

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]

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