refl — Mathlib

English

Let α be a type. There exists a canonical equivalence α ≃ α whose forward and inverse maps are the identity function; this is the identity equivalence.

Русский

Пусть α — множество. Существует каноническая эквивалентность α ≃ α, заданная тождественным отображением; переход и обратное отображение являются тождественными отображениями.

LaTeX

$$$\exists e:\alpha \simeq \alpha,\ e.toFun = \mathrm{id}_\alpha \land e.invFun = \mathrm{id}_\alpha$$$

Lean4

/-- Any type is equivalent to itself. -/
@[refl]
protected def refl (α : Sort*) : α ≃ α :=
  ⟨id, id, fun _ => rfl, fun _ => rfl⟩

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