rec_heq_of_heq — Mathlib

English

If a = b and x ≍ y, then transporting x along the equality a = b yields an equal heterogeneous relation with y.

Русский

Если a = b и x ≍ y, то перенос x по равенству a = b сохраняет гетерогенное равенство с y.

LaTeX

$$$e: a=b,\\ h: x \\overset{HEq}{\\sim} y \\Rightarrow e\\\\, x \\\\overset{HEq}{\\sim} y$$$

Lean4

theorem rec_heq_of_heq {α β : Sort _} {a b : α} {C : α → Sort*} {x : C a} {y : β} (e : a = b) (h : x ≍ y) : e ▸ x ≍ y :=
  eqRec_heq_iff_heq.mpr h

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