nddcongrArg

Mathlib.Tactic.DepRewrite

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.DepRewrite.nddcongrArg

Lean4

theorem nddcongrArg.{u, v} {α : Sort u} {a a' : α} {β : Sort v} (h : a = a') (f : (a' : α) → (h : a = a') → β) :
    f a rfl = f a' h := by cases h; rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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