heq_iff_exists_cast_eq — Mathlib

English

A heterogeneous equality a ≍ b holds iff there exists an isomorphism h: α = β such that cast h a = b.

Русский

Гетерогенное равенство a ≍ b эквивалентно существованию h: α = β, такого что cast h a = b.

LaTeX

$$$a\\\\overset{HEq}{\\\\sim} b\\\\iff\\\\exists h:\\\\alpha=\\\\beta, cast h a = b$$$

Lean4

theorem heq_iff_exists_cast_eq : a ≍ b ↔ ∃ (h : α = β), cast h a = b := by
  simp only [heq_comm (a := a), heq_iff_exists_eq_cast, eq_comm]

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