uniformEquiv_mk_coe

Mathlib.Topology.UniformSpace.Equiv

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

English

The function part of a constructed uniform equivalence is exactly the given equivalence.

Русский

Функциональная часть сконструированного UniformEquiv совпадает с данным эквивалентностью.

LaTeX

$$$(UniformEquiv.mk a b c : \alpha \to \beta) = a$$$

Lean4

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

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

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

Разделы

Аффилиация

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