union_pi_inter — Mathlib

English

If t1_i and t2_i are univ outside s1 and s2, then (s1 ∪ s2).pi (t1 i ∩ t2 i) equals s1.pi t1 ∩ s2.pi t2.

Русский

Если вне s1 и s2 элементы t1_i и t2_i равны всевозможным, то произведение по объединению равно пересечению произведений по частям.

LaTeX

$$$ (s_1 \cup s_2).\pi (i \mapsto t_1 i \cap t_2 i) = s_1.\pi t_1 \cap s_2.\pi t_2 $$$

Lean4

theorem union_pi_inter (ht₁ : ∀ i ∉ s₁, t₁ i = univ) (ht₂ : ∀ i ∉ s₂, t₂ i = univ) :
    (s₁ ∪ s₂).pi (fun i ↦ t₁ i ∩ t₂ i) = s₁.pi t₁ ∩ s₂.pi t₂ := by grind

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