coe_symm_toEquiv

Mathlib.Topology.UniformSpace.Equiv

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

English

If two uniform equivalences have the same underlying equivalence, then they are equal.

Русский

Если две равномерно эквивалентности имеют одинаковое базовое эквивалентное отображение, то они равны.

LaTeX

$$toEquiv инъективен: ∀ a b, toEquiv(a)=toEquiv(b) → a=b$$

Lean4

@[simp]
theorem coe_symm_toEquiv (h : α ≃ᵤ β) : ⇑h.toEquiv.symm = h.symm :=
  rfl

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

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

Разделы

Аффилиация

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