English
Let s : α ⊕ β → Set γ. Then the intersection over the sum equals the intersection of the two intersections: ⋂ x, s x = (⋂ x, s (Sum.inl x)) ∩ (⋂ x, s (Sum.inr x)).
Русский
Пусть s : α ⊕ β → Set γ. Тогда пересечение по сумме равно пересечению двух пересечений: ⋂ x, s x = (⋂ x, s (Sum.inl x)) ∩ (⋂ x, s (Sum.inr x)).
LaTeX
$$$$\\bigcap_{x} s(x) = \\Bigl(\\bigcap_{x} s(\\mathrm{Sum.inl}\\, x)\\Bigr) \\cap \\Bigl(\\bigcap_{x} s(\\mathrm{Sum.inr}\\, x)\\Bigr).$$$$
Lean4
theorem iInter_sum {s : α ⊕ β → Set γ} : ⋂ x, s x = (⋂ x, s (.inl x)) ∩ ⋂ x, s (.inr x) :=
iInf_sum