default_coe_singleton — Mathlib

English

The unique element of the singleton {x} (viewed as a subset of α) corresponds to x itself; i.e., the canonical element of the singleton subtype is x.

Русский

Единственный элемент множества-одиночки {x} соответствует самому x; т. е. канонический элемент подтипа единичного множества равен x.

LaTeX

$$$\text{default}_{\{x\}} = \langle x, rfl \rangle$$$

Lean4

@[simp]
theorem default_coe_singleton (x : α) : (default : ({ x } : Set α)) = ⟨x, rfl⟩ :=
  rfl

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