prod_sInter — Mathlib

English

The product with an sInter equals the intersection over s ∈ S of s × t, provided S is nonempty.

Русский

Произведение с пересечением равно пересечению по элементам, если S непусто.

LaTeX

$$$s \times\!\bigcap_{t \in T} t = \bigcap_{t \in T} (s \times t)$$$

Lean4

theorem prod_sInter {T : Set (Set β)} (hT : T.Nonempty) (s : Set α) : s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t :=
  by
  rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton]
  simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

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