cast_eq_iff_heq

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.cast_eq_iff_heq

English

For h: α = β, the equation cast h a = b is equivalent to a being heterogeneous equal to b (HEq).

Русский

Для h: α = β, равенство cast h a = b эквивалентно гетерогенно-эквивалентному a и b (HEq).

LaTeX

$$$(\\mathrm{cast}(h)\\,a = b) \\iff a \\;\\overset{HEq}\\sim\\; b.$$$

Lean4

theorem cast_eq_iff_heq {α β} (h : α = β) {a : α} {b : β} : Equiv.cast h a = b ↔ a ≍ b := by subst h; simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru