continuousMapOfUnique_symm_apply

Mathlib.Topology.CompactOpen

URI: https://scilib.ai/kg/mathlib#Homeomorph.continuousMapOfUnique_symm_apply

English

The symmetric application gives that the inverse of the unique-map sends f to f(default).

Русский

Обратное отображение единственного отображения возвращает f(по умолчанию).

LaTeX

$$$\\mathrm{continuousMapOfUnique}.symm f = f(\\text{default})$$$

Lean4

@[simp]
theorem continuousMapOfUnique_symm_apply [Unique X] (f : C(X, Y)) : continuousMapOfUnique.symm f = f default :=
  rfl

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

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

Разделы

Аффилиация

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