eq

Mathlib.Data.Sigma.Basic

URI: https://scilib.ai/kg/mathlib#Sigma.eq

Lean4

protected theorem eq {α : Type*} {β : α → Type*} :
    ∀ {p₁ p₂ : Σ a, β a} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
  | ⟨_, _⟩, _, rfl, rfl => rfl

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

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

Разделы

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

Аффилиация

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