disjoin_manyOneReducible — Mathlib

English

If p ≤₀ r and q ≤₀ r, then p ⊕' q ≤₀ r.

Русский

Если p и q обе редуцируются к r, то сумма p ⊕' q редуцируется к r.

LaTeX

$$$ p \\le_0 r \\to q \\le_0 r \\to (p \\oplus' q) \\le_0 r $$$

Lean4

theorem disjoin_manyOneReducible {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop}
    {r : γ → Prop} : p ≤₀ r → q ≤₀ r → (p ⊕' q) ≤₀ r
  | ⟨f, c₁, h₁⟩, ⟨g, c₂, h₂⟩ =>
    ⟨Sum.elim f g, Computable.id.sumCasesOn (c₁.comp Computable.snd).to₂ (c₂.comp Computable.snd).to₂, fun x => by
      cases x <;> [apply h₁; apply h₂]⟩

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