single_subsingleton_eq_refl — Mathlib

English

If α is a Subsingleton, then for any a, b ∈ α, single a b = refl α.

Русский

Если α — множество-один, тогда для любых a, b ∈ α, single a b = refl α.

LaTeX

$$[Subsingleton α] (a b : α) : single a b = PEquiv.refl α$$

Lean4

@[simp]
theorem single_subsingleton_eq_refl [Subsingleton α] (a b : α) : single a b = PEquiv.refl α :=
  by
  ext i j
  dsimp [single]
  rw [if_pos (Subsingleton.elim i a), Subsingleton.elim i j, Subsingleton.elim b j]

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