English
Let b : β, p : β → Prop, and s : ∀ x : β, x = b ∨ p x → Set α. Then the intersection over x of s x h equals s b (Or.inl rfl) ∩ ⋂ x (h : p x), s x (Or.inr h).
Русский
Пусть b : β, p : β → Prop и s : ∀ x : β, x = b ∨ p x → Set α. Тогда пересечение по x: s x h равно s b (Or.inl rfl) ∩ ⋂ x (h : p x), s x (Or.inr h).
LaTeX
$$$$\\bigcap_{x} s(x,h) = s\\big(b,\\mathrm{Or.inl}(\\mathrm{rfl})\\big) \\;\\cap\\; \\bigcap_{x} \\bigl\\{ s\\big(x,\\mathrm{Or.inr}(h)\\bigr) : h \\in p(x) \\bigr\\}. $$$$
Lean4
@[simp]
theorem iInter_iInter_eq_or_left {b : β} {p : β → Prop} {s : ∀ x : β, x = b ∨ p x → Set α} :
⋂ (x) (h), s x h = s b (Or.inl rfl) ∩ ⋂ (x) (h : p x), s x (Or.inr h) := by
simp only [iInter_or, iInter_inter_distrib, iInter_iInter_eq_left]
