toNat_congr — Mathlib

English

If e is an equivalence α ≃ β, then toNat(#α) = toNat(#β).

Русский

Если e — эквивалентность α ≃ β, то toNat(#α) = toNat(#β).

LaTeX

$$$\forall {\alpha,\beta},\; (e: \alpha \simeq \beta) \Rightarrow toNat(#\alpha) = toNat(#\beta).$$$

Lean4

theorem toNat_congr {β : Type v} (e : α ≃ β) : toNat #α = toNat #β := by
  -- Porting note: Inserted universe hint below
  rw [← toNat_lift, (lift_mk_eq.{_, _, v}).mpr ⟨e⟩, toNat_lift]

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