English
Let b : β, p : β → Prop, and s : ∀ x : β, x = b ∨ p x → Set α. Then the union 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
$$$$\\bigcup_{x} s(x,h) = s\\big(b,\\mathrm{Or.inl}(\\mathrm{rfl})\\big) \\;\\cup\\; \\bigcup_{x} \\bigl\\{ s\\big(x,\\mathrm{Or.inr}(h)\\big) : h \\in p(x) \\bigr\\}. $$$$
Lean4
@[simp]
theorem iUnion_iUnion_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 [iUnion_or, iUnion_union_distrib, iUnion_iUnion_eq_left]
