English
Reducibility of a disjoint sum to r is equivalent to reducibility of each component to r.
Русский
Редукционируемость Sum.elim p q к r эквивалентна редукционируемости p к r и q к r.
LaTeX
$$$ \\ManyOneReducible (\\mathrm{Sum.elim}\ p\\ q)\\ r \\iff (\\ManyOneReducible p r) \\land (\\ManyOneReducible q r) $$$
Lean4
theorem disjoin_le {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop}
{r : γ → Prop} : (p ⊕' q) ≤₀ r ↔ p ≤₀ r ∧ q ≤₀ r :=
⟨fun h => ⟨OneOneReducible.disjoin_left.to_many_one.trans h, OneOneReducible.disjoin_right.to_many_one.trans h⟩,
fun ⟨h₁, h₂⟩ => disjoin_manyOneReducible h₁ h₂⟩
