trans — Mathlib

English

If e1: α ≃ β and e2: β ≃ γ are computable, then their composition is computable.

Русский

Если e1: α ≃ β и e2: β ≃ γ вычислимы, то их композиция вычислима.

LaTeX

$$$\forall e_1:\alpha\simeq\beta, e_2:\beta\simeq\gamma,\ e_1.Computable\to e_2.Computable\to (e_1.trans e_2).Computable$$$

Lean4

@[trans]
theorem trans {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :
    OneOneEquiv p q → OneOneEquiv q r → OneOneEquiv p r
  | ⟨pq, qp⟩, ⟨qr, rq⟩ => ⟨pq.trans qr, rq.trans qp⟩

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