sInter_prod_sInter — Mathlib

English

If both S and T are nonempty, the product of their intersections equals the intersection over the cross product of the members.

Русский

Если S и T непусты, произведение пересечений равно пересечению по парам.

LaTeX

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

Lean4

theorem sInter_prod_sInter {S : Set (Set α)} {T : Set (Set β)} (hS : S.Nonempty) (hT : T.Nonempty) :
    ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2 := by
  obtain ⟨s₁, h₁⟩ := hS
  obtain ⟨s₂, h₂⟩ := hT
  refine Set.Subset.antisymm (sInter_prod_sInter_subset S T) fun x hx => ?_
  rw [mem_iInter₂] at hx
  exact ⟨fun s₀ h₀ => (hx (s₀, s₂) ⟨h₀, h₂⟩).1, fun s₀ h₀ => (hx (s₁, s₀) ⟨h₁, h₀⟩).2⟩

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