ofEquiv_ofNat — Mathlib

English

For any e : β ≃ α, and n, the ofNat on β equals the inverse of e applied to ofNat on α: ofNat β n = e^{-1}(ofNat α n).

Русский

Для любого e : β ≃ α и любого n, ofNat β n = e^{-1}(ofNat α n).

LaTeX

$$$ @ofNat \beta (ofEquiv _ e) n = e^{-1}(ofNat \alpha n) $$$

Lean4

@[simp]
theorem ofEquiv_ofNat (α) {β} [Denumerable α] (e : β ≃ α) (n) : @ofNat β (ofEquiv _ e) n = e.symm (ofNat α n) :=
  by
  letI := ofEquiv _ e
  refine ofNat_of_decode ?_
  rw [decode_ofEquiv e]
  simp

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