ofEquiv — Mathlib

English

Encodability is preserved by equivalence: if α is encodable and e: β ≃ α, then β is encodable via ofEquiv.

Русский

Кодируемость сохраняется при эквивалентности: если α кодируем, и e: β ≃ α, то β кодируем через ofEquiv.

LaTeX

$$$\text{Encodable}(\beta,\text{ofEquiv}(\alpha,e))$$$

Lean4

/-- Encodability is preserved by equivalence. -/
def ofEquiv (α) [Encodable α] (e : β ≃ α) : Encodable β :=
  ofLeftInverse e e.symm e.left_inv

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