symm_castOrderIso — Mathlib

English

The inverse of castOrderIso is castOrderIso of the reversed equality: (castOrderIso h).symm = castOrderIso h.symm.

Русский

Обратное к castOrderIso отображение равно castOrderIso от обратного равенства: (castOrderIso h).symm = castOrderIso h.symm.

LaTeX

$$$\forall {n m : \mathbb{N}} (h : n = m), (castOrderIso h).symm = castOrderIso h.symm$$$

Lean4

@[simp]
theorem symm_castOrderIso (h : n = m) : (castOrderIso h).symm = castOrderIso h.symm := by subst h; rfl

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