of_equiv — Mathlib

English

If e is a computable equivalence between α and β, then the predicate q on β reduces to q on α via composition with e.

Русский

Если e — вычислимая эквивалентность между α и β, то предикат q на β редуцируется к q через композицию с e.

LaTeX

$$$\forall \alpha\beta\,[Primcodable\ \alpha]\,[Primcodable\ \beta]\{e:\alpha\simeq\beta\}\ (q:\beta\to\mathrm{Prop})\to (q\circ e)\le_1 q$$$

Lean4

theorem of_equiv {α β} [Primcodable α] [Primcodable β] {e : α ≃ β} (q : β → Prop) (h : Computable e) : (q ∘ e) ≤₁ q :=
  OneOneReducible.mk _ h e.injective

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