trans — Mathlib

English

If e1 and e2 are computable equivalences, then their composition is computable.

Русский

Если e1 и e2 вычислимые эквивалентности, то их композиция вычислима.

LaTeX

$$$e_1.Computable \land e_2.Computable \Rightarrow (e_1.trans e_2).Computable$$$

Lean4

theorem trans {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {e₁ : α ≃ β} {e₂ : β ≃ γ} :
    e₁.Computable → e₂.Computable → (e₁.trans e₂).Computable
  | ⟨l₁, r₁⟩, ⟨l₂, r₂⟩ => ⟨l₂.comp l₁, r₁.comp r₂⟩

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