funUnique_symm_apply — Mathlib

English

If α has a unique element and β is preordered, then the inverse of funUnique α β is the constant function α → β.

Русский

Если у α есть ровно один элемент, а β — предорудованный, то обратное отображение funUnique α β равно константной функции α → β.

LaTeX

$$$ ((\text{funUnique }\alpha\beta)^{\mathrm{symm}} : \beta \to (\alpha \to \beta)) = \text{Function.const } \alpha$$$

Lean4

@[simp]
theorem funUnique_symm_apply {α β : Type*} [Unique α] [Preorder β] :
    ((funUnique α β).symm : β → α → β) = Function.const α :=
  rfl

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