iInter_sum — Mathlib

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

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