prod_inter_prod — Mathlib

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]

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