English
Let p be a predicate on functions γ : α ⊕ β → Sort*. Then there exists a function fab with property p fab iff there exist fa : α → Sort*, fb : β → Sort* with p (Sum.rec fa fb).
Русский
Пусть p зависит от функции γ : α ⊕ β → Sort*. Тогда существует функция fab такая, что p fab, эквивалентно тому, что существуют fa : α → Sort*, fb : β → Sort* с p( Sum.rec fa fb ).
LaTeX
$$$\\exists f : (\\alpha \\oplus \\beta) \\to \\mathrm{Sort},\\ p\; f \iff \\exists a : \\alpha \\to \\mathrm{Sort},\\exists b : \\beta \\to \\mathrm{Sort},\\ p(\\mathrm{Sum.rec}\\ a\\ b).$$$
Lean4
theorem exists_sum {γ : α ⊕ β → Sort*} (p : (∀ ab, γ ab) → Prop) : (∃ fab, p fab) ↔ (∃ fa fb, p (Sum.rec fa fb)) :=
by
rw [← not_forall_not, forall_sum]
simp
