coe_mk

Mathlib.Topology.MetricSpace.Isometry

URI: https://scilib.ai/kg/mathlib#IsometryEquiv.coe_mk

English

If you build an isometry equivalence from an equivalence e and a proof h, the underlying function is e.

Русский

Построенная из эквивалентности e и доказательства h изометрическая эквивалентность имеет базовую функцию e.

LaTeX

$$$ \forall x, \ (\mathrm{mk}(e,h))(x) = e(x). $$$

Lean4

@[simp]
theorem coe_mk (e : α ≃ β) (h) : ⇑(mk e h) = e :=
  rfl

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

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

Разделы

Аффилиация

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