iInter_or — Mathlib

English

The overall intersection over Or p q decomposes into the intersection over p and the intersection over q.

Русский

Общее пересечение по Or p q распадается на пересечение по p и пересечение по q.

LaTeX

$$$$\\bigcap_h s_h = (\\bigcap_{h: p} s_{Or.inl h}) \\cap (\\bigcap_{h: q} s_{Or.inr h})$$$$

Lean4

theorem iInter_or {p q : Prop} (s : p ∨ q → Set α) : ⋂ h, s h = (⋂ h : p, s (Or.inl h)) ∩ ⋂ h : q, s (Or.inr h) :=
  iInf_or

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