pi_inter_distrib — Mathlib

English

The pi over t of intersections distributes over intersection: (s.pi t) ∩ (s.pi t₁) = s.pi (i ↦ t i ∩ t₁ i).

Русский

Произведение по s от пересечения распределяется по пересечению: (s.pi t) ∩ (s.pi t₁) = s.pi (i ↦ t i ∩ t₁ i).

LaTeX

$$$ (s.pi \!\; t) \cap (s.pi \!\; t₁) = s.pi (\lambda i. t i \cap t₁ i) $$$

Lean4

theorem pi_inter_distrib : (s.pi fun i => t i ∩ t₁ i) = s.pi t ∩ s.pi t₁ := by grind

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