sigma_inter_sigma — Mathlib

English

Let s1, s2 ⊆ ι and t1, t2: ∀ i, Set(α(i)). Then the intersection of s1.sigma t1 and s2.sigma t2 equals (s1 ∩ s2).sigma (i ↦ t1(i) ∩ t2(i)).

Русский

Пусть s1, s2 ⊆ ι и t1, t2: для каждого i задано множество t1(i), t2(i) ⊆ α(i). Тогда пересечение s1.sigma t1 и s2.sigma t2 равняется (s1 ∩ s2).sigma (i ↦ t1(i) ∩ t2(i)).

LaTeX

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

Lean4

theorem sigma_inter_sigma : s₁.sigma t₁ ∩ s₂.sigma t₂ = (s₁ ∩ s₂).sigma fun i ↦ t₁ i ∩ t₂ i := by grind

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