English
The product of intersections equals the intersection of products: (s1 × t1) ∩ (s2 × t2) = (s1 ∩ s2) × (t1 ∩ t2).
Русский
Произведение пересечений равно пересечению произведений: (s1 × t1) ∩ (s2 × t2) = (s1 ∩ s2) × (t1 ∩ t2).
LaTeX
$$$ (s_1 \times t_1) \cap (s_2 \times t_2) = (s_1 \cap s_2) \times (t_1 \cap t_2) $$$
Lean4
@[mfld_simps]
theorem prod_inter_prod : s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) :=
by
ext ⟨x, y⟩
simp [and_assoc, and_left_comm]