cast_apply

Mathlib.Logic.Equiv.Defs

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

English

If h: α = β, then cast h x = cast h x; a trivial definitional equality.

Русский

Если h: α = β, то cast h x = cast h x; тривиальное определение равенства.

LaTeX

$$$\\mathrm{cast}(h)\\,x = \\mathrm{cast}(h)\\,x$$$

Lean4

@[simp]
theorem cast_apply {α β} (h : α = β) (x : α) : Equiv.cast h x = cast h x :=
  rfl

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

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

Разделы

Аффилиация

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