decode_ofEquiv — Mathlib

English

Decoding through an equivalence corresponds to decoding in the target and mapping back via the inverse equivalence.

Русский

Декодирование через эквивалентность соответствует декодированию в целевом типе и обратному отображению через симм-эквиваленцию.

LaTeX

$$$\operatorname{decode}_{\text{ofEquiv}(\alpha,e)}(n) = (\operatorname{decode} n).map (e^{-1})$$$

Lean4

theorem decode_ofEquiv {α β} [Encodable α] (e : β ≃ α) (n : ℕ) : @decode _ (ofEquiv _ e) n = (decode n).map e.symm :=
  show Option.bind _ _ = Option.map _ _ by rw [Option.map_eq_bind]

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