uniformEquiv_mk_coe_symm

Mathlib.Topology.UniformSpace.Equiv

URI: https://scilib.ai/kg/mathlib#UniformEquiv.uniformEquiv_mk_coe_symm

English

The coefficient of a UniformEquiv.mk is the underlying equivalence.

Русский

Коэффициент UniformEquiv.mk равен базовой эквиваленции.

LaTeX

$$(UniformEquiv.mk a b c : α → β) = a$$

Lean4

@[simp]
theorem uniformEquiv_mk_coe_symm (a : Equiv α β) (b c) : ((UniformEquiv.mk a b c).symm : β → α) = a.symm :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru