of_equiv_symm — Mathlib

English

If e.symm is computable, then q is reducible to q∘e via one-one reduction.

Русский

Если e.symm вычислима, то q редуцируется к q∘e с помощью однозначной редукции.

LaTeX

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

Lean4

theorem of_equiv_symm {α β} [Primcodable α] [Primcodable β] {e : α ≃ β} (q : β → Prop) (h : Computable e.symm) :
    q ≤₁ (q ∘ e) := by convert OneOneReducible.of_equiv _ h; funext; simp

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