subsingleton_unique' — Mathlib

English

For any two elements h1,h2 of Unique α, we have h1 = h2; the type Unique α is a subsingleton.

Русский

Для любых двух элементов h1,h2 типа Unique α выполняется h1 = h2; тип Unique α является пододиночным.

LaTeX

$$∀ h1 h2 : Unique α, h1 = h2$$

Lean4

@[ext]
protected theorem subsingleton_unique' : ∀ h₁ h₂ : Unique α, h₁ = h₂
  | ⟨⟨x⟩, h⟩, ⟨⟨y⟩, _⟩ => by congr; rw [h x, h y]

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