decidableEqOfEncodable — 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

/-- An encodable type has decidable equality. Not set as an instance because this is usually not the
best way to infer decidability. -/
def decidableEqOfEncodable (α) [Encodable α] : DecidableEq α
  | _, _ => decidable_of_iff _ encode_inj

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