English
Let p, q, r be predicates on α, β, γ (with Primcodable domains). If p reduces to q via a computable injective map and q reduces to r via another computable injective map, then p reduces to r via the composition of those maps.
Русский
Пусть p, q, r — предикаты на α, β, γ (с областями, кодируемыми примитивно). Если p редуцируется к q по вычислимому инъективному отображению, а q редуцируется к r по вычислимому инъективному отображению, то p редуцируется к r композицией этих отображений.
LaTeX
$$$\forall \alpha\,\beta\,\gamma\ ([Primcodable\ \alpha])\,[Primcodable\ \beta]\,[Primcodable\ \gamma]\;\{p:\alpha\to\mathrm{Prop}\}\{q:\beta\to\mathrm{Prop}\}\{r:\gamma\to\mathrm{Prop}\},\; p\le_1 q\;\land\; q\le_1 r\;\Rightarrow\; p\le_1 r$$$
Lean4
@[trans]
theorem trans {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :
p ≤₁ q → q ≤₁ r → p ≤₁ r
| ⟨f, c₁, i₁, h₁⟩, ⟨g, c₂, i₂, h₂⟩ =>
⟨g ∘ f, c₂.comp c₁, i₂.comp i₁, fun a =>
⟨fun h => by rw [comp_apply, ← h₂, ← h₁]; assumption, fun h => by rwa [h₁, h₂]⟩⟩
