prod_iInter — Mathlib

English

The product distributes with a big intersection: (s ×ˢ ⋂ i, t i) = ⋂ i, s ×ˢ t i, under Nonempty ι.

Русский

Произведение распределяется через большую пересечение: (s ×ˢ ⋂ i, t_i) = ⋂ i, s ×ˢ t_i, при непустой индексации.

LaTeX

$$$(s \times\! \bigcap_i t_i) = \bigcap_i (s \times t_i)$$$

Lean4

theorem prod_iInter {s : Set α} {t : ι → Set β} [hι : Nonempty ι] : (s ×ˢ ⋂ i, t i) = ⋂ i, s ×ˢ t i :=
  by
  ext x
  simp only [mem_prod, mem_iInter]
  exact ⟨fun h i => ⟨h.1, h.2 i⟩, fun h => ⟨(h hι.some).1, fun i => (h i).2⟩⟩

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